![]() |
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 form). (Contributed by NM, 28-Jan-2006.) |
Ref | Expression |
---|---|
2rexbidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
2rexbidv | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2rexbidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | rexbidv 3237 | . 2 ⊢ (𝜑 → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | rexbidv 3237 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∃wrex 3091 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1824 df-rex 3096 |
This theorem is referenced by: f1oiso 6875 elrnmpt2g 7051 elrnmpt2 7052 ralrnmpt2 7054 ovelrn 7089 opiota 7510 omeu 7951 oeeui 7968 eroveu 8128 erov 8130 elfiun 8626 dffi3 8627 xpwdomg 8781 brdom7disj 9690 brdom6disj 9691 genpv 10158 genpelv 10159 axcnre 10323 supadd 11349 supmullem1 11351 supmullem2 11352 supmul 11353 sqrlem6 14399 ello1 14658 ello1mpt 14664 elo1 14669 lo1o1 14675 o1lo1 14680 bezoutlem1 15666 bezoutlem3 15668 bezoutlem4 15669 bezout 15670 pythagtriplem2 15930 pythagtriplem19 15946 pythagtrip 15947 pcval 15957 pceu 15959 pczpre 15960 pcdiv 15965 4sqlem2 16061 4sqlem3 16062 4sqlem4 16064 4sq 16076 vdwlem1 16093 vdwlem12 16104 vdwlem13 16105 vdwnnlem1 16107 vdwnnlem2 16108 vdwnnlem3 16109 vdwnn 16110 ramub2 16126 rami 16127 pgpfac1lem3 18867 lspprel 19493 znunit 20311 cayleyhamiltonALT 21107 hausnei 21544 isreg2 21593 txuni2 21781 txbas 21783 xkoopn 21805 txcls 21820 txcnpi 21824 txdis1cn 21851 txtube 21856 txcmplem1 21857 hausdiag 21861 tx1stc 21866 regr1lem2 21956 qustgplem 22336 met2ndci 22739 dyadmax 23806 i1fadd 23903 i1fmul 23904 elply 24392 2sqlem2 25599 2sqlem8 25607 2sqlem9 25608 2sqlem11 25610 istrkgld 25814 axtgeucl 25827 legov 25940 iscgra 26161 dfcgra2 26182 axsegconlem1 26270 axpasch 26294 axlowdim 26314 axeuclidlem 26315 nb3grpr 26734 upgr4cycl4dv4e 27592 vdgn1frgrv2 27708 fusgr2wsp2nb 27746 l2p 27910 br8d 29989 pstmval 30540 eulerpartlemgh 31042 eulerpartlemgs2 31044 cvmliftlem15 31883 cvmlift2lem10 31897 br8 32244 br6 32245 br4 32246 elaltxp 32675 brsegle 32808 ellines 32852 nn0prpwlem 32909 nn0prpw 32910 ptrest 34039 ismblfin 34081 itg2addnclem3 34093 itg2addnc 34094 isline 35898 psubspi 35906 paddfval 35956 elpadd 35958 paddvaln0N 35960 3rspcedvd 38125 mzpcompact2lem 38284 mzpcompact2 38285 sbc4rexgOLD 38324 pell1qrval 38380 elpell1qr 38381 pell14qrval 38382 elpell14qr 38383 pell1234qrval 38384 elpell1234qr 38385 jm2.27 38544 expdiophlem1 38557 clsk1independent 39310 limclner 40801 fourierdlem42 41303 fourierdlem48 41308 sprel 42433 prelspr 42435 prprelb 42465 prprelprb 42466 isgbe 42674 isgbow 42675 isgbo 42676 sbgoldbalt 42704 sgoldbeven3prm 42706 mogoldbb 42708 sbgoldbo 42710 nnsum3primesle9 42717 bigoval 43368 elbigo 43370 |
Copyright terms: Public domain | W3C validator |