![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2rexbidv | Structured version Visualization version GIF version |
Description: Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.) |
Ref | Expression |
---|---|
2rexbidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
2rexbidv | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2rexbidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | rexbidv 3081 | . 2 ⊢ (𝜑 → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | rexbidv 3081 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∃wrex 2942 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1745 df-rex 2947 |
This theorem is referenced by: f1oiso 6641 elrnmpt2g 6814 elrnmpt2 6815 ralrnmpt2 6817 ovelrn 6852 opiota 7273 omeu 7710 oeeui 7727 eroveu 7885 erov 7887 elfiun 8377 dffi3 8378 xpwdomg 8531 brdom7disj 9391 brdom6disj 9392 genpv 9859 genpelv 9860 axcnre 10023 supadd 11029 supmullem1 11031 supmullem2 11032 supmul 11033 sqrlem6 14032 ello1 14290 ello1mpt 14296 elo1 14301 lo1o1 14307 o1lo1 14312 bezoutlem1 15303 bezoutlem3 15305 bezoutlem4 15306 bezout 15307 pythagtriplem2 15569 pythagtriplem19 15585 pythagtrip 15586 pcval 15596 pceu 15598 pczpre 15599 pcdiv 15604 4sqlem2 15700 4sqlem3 15701 4sqlem4 15703 4sq 15715 vdwlem1 15732 vdwlem12 15743 vdwlem13 15744 vdwnnlem1 15746 vdwnnlem2 15747 vdwnnlem3 15748 vdwnn 15749 ramub2 15765 rami 15766 pgpfac1lem3 18522 lspprel 19142 znunit 19960 cayleyhamiltonALT 20744 hausnei 21180 isreg2 21229 txuni2 21416 txbas 21418 xkoopn 21440 txcls 21455 txcnpi 21459 txdis1cn 21486 txtube 21491 txcmplem1 21492 hausdiag 21496 tx1stc 21501 regr1lem2 21591 qustgplem 21971 met2ndci 22374 dyadmax 23412 i1fadd 23507 i1fmul 23508 elply 23996 2sqlem2 25188 2sqlem8 25196 2sqlem9 25197 2sqlem11 25199 istrkgld 25403 axtgeucl 25416 legov 25525 iscgra 25746 dfcgra2 25766 axsegconlem1 25842 axpasch 25866 axlowdim 25886 axeuclidlem 25887 nb3grpr 26328 upgr4cycl4dv4e 27163 vdgn1frgrv2 27276 fusgr2wsp2nb 27314 l2p 27461 br8d 29548 pstmval 30066 eulerpartlemgh 30568 eulerpartlemgs2 30570 cvmliftlem15 31406 cvmlift2lem10 31420 br8 31772 br6 31773 br4 31774 elaltxp 32207 brsegle 32340 ellines 32384 nn0prpwlem 32442 nn0prpw 32443 ptrest 33538 ismblfin 33580 itg2addnclem3 33593 itg2addnc 33594 isline 35343 psubspi 35351 paddfval 35401 elpadd 35403 paddvaln0N 35405 mzpcompact2lem 37631 mzpcompact2 37632 sbc4rexgOLD 37671 pell1qrval 37727 elpell1qr 37728 pell14qrval 37729 elpell14qr 37730 pell1234qrval 37731 elpell1234qr 37732 jm2.27 37892 expdiophlem1 37905 clsk1independent 38661 limclner 40201 fourierdlem42 40684 fourierdlem48 40689 isgbe 41964 isgbow 41965 isgbo 41966 sbgoldbalt 41994 sgoldbeven3prm 41996 mogoldbb 41998 sbgoldbo 42000 nnsum3primesle9 42007 sprel 42059 prelspr 42061 bigoval 42668 elbigo 42670 |
Copyright terms: Public domain | W3C validator |