![]() |
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 667 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓)) |
3 | 2 | rexbii2 3021 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∈ wcel 1977 ∃wrex 2897 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-rex 2902 |
This theorem is referenced by: 2rexbiia 3037 ceqsrexbv 3307 reu8 3369 f1oweALT 7043 reldm 7110 seqomlem2 7433 fofinf1o 8126 wdom2d 8368 unbndrank 8588 cfsmolem 8975 fin1a2lem5 9109 fin1a2lem6 9110 infm3 10861 wwlktovfo 13549 even2n 14904 znf1o 19719 lmres 20914 ist1-2 20961 itg2monolem1 23323 lhop1lem 23580 elaa 23875 ulmcau 23953 reeff1o 24005 recosf1o 24085 chpo1ubb 24970 istrkg2ld 25159 wlknwwlknsur 26240 wlkiswwlksur 26247 wwlkextsur 26259 nmopnegi 28208 nmop0 28229 nmfn0 28230 adjbd1o 28328 atom1d 28596 abfmpunirn 28832 rearchi 29173 eulerpartgbij 29761 eulerpartlemgh 29767 subfacp1lem3 30418 dfrdg2 30945 heiborlem7 32786 eq0rabdioph 36358 elicores 38607 fourierdlem70 39069 fourierdlem80 39079 ovolval3 39537 rexrsb 39818 1wlkpwwlkf1ouspgr 41076 wlknwwlksnsur 41087 wlkwwlksur 41094 wwlksnextsur 41106 |
Copyright terms: Public domain | W3C validator |