![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexbiia | Structured version Visualization version GIF version |
Description: Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 26-Oct-1999.) |
Ref | Expression |
---|---|
rexbiia.1 | ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
rexbiia | ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexbiia.1 | . . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) | |
2 | 1 | pm5.32i 576 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓)) |
3 | 2 | rexbii2 3090 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∈ wcel 2107 ∃wrex 3070 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-rex 3071 |
This theorem is referenced by: rexbii 3094 rexanid 3096 2rexbiia 3206 ceqsrexbv 3607 reu8 3692 f1oweALT 7906 reldm 7977 seqomlem2 8398 fofinf1o 9274 wdom2d 9521 unbndrank 9783 cfsmolem 10211 fin1a2lem5 10345 fin1a2lem6 10346 infm3 12119 wwlktovfo 14853 even2n 16229 smndex1mnd 18725 cycsubmel 18998 znf1o 20974 lmres 22667 ist1-2 22714 itg2monolem1 25131 lhop1lem 25393 elaa 25692 ulmcau 25770 reeff1o 25822 recosf1o 25907 chpo1ubb 26845 noetainflem4 27104 istrkg2ld 27444 wlkswwlksf1o 28866 wwlksnextsurj 28887 nmopnegi 30949 nmop0 30970 nmfn0 30971 adjbd1o 31069 atom1d 31337 abfmpunirn 31614 rearchi 32185 eulerpartgbij 33029 eulerpartlemgh 33035 subfacp1lem3 33833 dfrdg2 34426 heiborlem7 36322 qsresid 36832 eq0rabdioph 41142 elicores 43857 liminfpnfuz 44143 xlimpnfxnegmnf2 44185 fourierdlem70 44503 fourierdlem80 44513 ovolval3 44974 rexrsb 45418 |
Copyright terms: Public domain | W3C validator |