![]() |
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 573 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓)) |
3 | 2 | rexbii2 3087 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∈ wcel 2098 ∃wrex 3067 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-rex 3068 |
This theorem is referenced by: rexbii 3091 rexanid 3093 2rexbiia 3213 ceqsrexbv 3644 reu8 3730 f1oweALT 7982 reldm 8054 seqomlem2 8478 fofinf1o 9359 wdom2d 9611 unbndrank 9873 cfsmolem 10301 fin1a2lem5 10435 fin1a2lem6 10436 infm3 12211 wwlktovfo 14949 even2n 16326 smndex1mnd 18869 cycsubmel 19162 znf1o 21492 lmres 23224 ist1-2 23271 itg2monolem1 25700 lhop1lem 25966 elaa 26271 ulmcau 26351 reeff1o 26404 recosf1o 26489 chpo1ubb 27434 noetainflem4 27693 0reno 28245 istrkg2ld 28284 wlkswwlksf1o 29710 wwlksnextsurj 29731 nmopnegi 31795 nmop0 31816 nmfn0 31817 adjbd1o 31915 atom1d 32183 abfmpunirn 32459 rearchi 33082 eulerpartgbij 34025 eulerpartlemgh 34031 subfacp1lem3 34825 dfrdg2 35424 heiborlem7 37323 qsresid 37829 cxpi11d 41945 eq0rabdioph 42227 elicores 44947 liminfpnfuz 45233 xlimpnfxnegmnf2 45275 fourierdlem70 45593 fourierdlem80 45603 ovolval3 46064 rexrsb 46509 |
Copyright terms: Public domain | W3C validator |