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 669 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓)) |
3 | 2 | rexbii2 3039 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∈ wcel 1990 ∃wrex 2913 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-rex 2918 |
This theorem is referenced by: 2rexbiia 3055 ceqsrexbv 3337 reu8 3402 f1oweALT 7152 reldm 7219 seqomlem2 7546 fofinf1o 8241 wdom2d 8485 unbndrank 8705 cfsmolem 9092 fin1a2lem5 9226 fin1a2lem6 9227 infm3 10982 wwlktovfo 13701 even2n 15066 znf1o 19900 lmres 21104 ist1-2 21151 itg2monolem1 23517 lhop1lem 23776 elaa 24071 ulmcau 24149 reeff1o 24201 recosf1o 24281 chpo1ubb 25170 istrkg2ld 25359 wlkpwwlkf1ouspgr 26765 wlknwwlksnsur 26776 wlkwwlksur 26783 wwlksnextsur 26795 nmopnegi 28824 nmop0 28845 nmfn0 28846 adjbd1o 28944 atom1d 29212 abfmpunirn 29452 rearchi 29842 eulerpartgbij 30434 eulerpartlemgh 30440 subfacp1lem3 31164 dfrdg2 31701 heiborlem7 33616 qsresid 34096 eq0rabdioph 37340 elicores 39760 fourierdlem70 40393 fourierdlem80 40403 ovolval3 40861 rexrsb 41169 |
Copyright terms: Public domain | W3C validator |