![]() |
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 3091 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∈ wcel 2107 ∃wrex 3071 |
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 3072 |
This theorem is referenced by: rexbii 3095 rexanid 3097 2rexbiia 3216 ceqsrexbv 3643 reu8 3728 f1oweALT 7954 reldm 8025 seqomlem2 8446 fofinf1o 9323 wdom2d 9571 unbndrank 9833 cfsmolem 10261 fin1a2lem5 10395 fin1a2lem6 10396 infm3 12169 wwlktovfo 14905 even2n 16281 smndex1mnd 18787 cycsubmel 19071 znf1o 21091 lmres 22786 ist1-2 22833 itg2monolem1 25250 lhop1lem 25512 elaa 25811 ulmcau 25889 reeff1o 25941 recosf1o 26026 chpo1ubb 26964 noetainflem4 27223 istrkg2ld 27691 wlkswwlksf1o 29113 wwlksnextsurj 29134 nmopnegi 31196 nmop0 31217 nmfn0 31218 adjbd1o 31316 atom1d 31584 abfmpunirn 31855 rearchi 32430 eulerpartgbij 33309 eulerpartlemgh 33315 subfacp1lem3 34111 dfrdg2 34705 heiborlem7 36623 qsresid 37132 eq0rabdioph 41447 elicores 44181 liminfpnfuz 44467 xlimpnfxnegmnf2 44509 fourierdlem70 44827 fourierdlem80 44837 ovolval3 45298 rexrsb 45743 |
Copyright terms: Public domain | W3C validator |