| 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 574 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓)) |
| 3 | 2 | rexbii2 3090 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∈ wcel 2108 ∃wrex 3070 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-rex 3071 |
| This theorem is referenced by: rexbii 3094 rexanid 3096 2rexbiia 3218 ceqsrexbv 3656 reu8 3739 f1oweALT 7997 reldm 8069 seqomlem2 8491 fofinf1o 9372 wdom2d 9620 unbndrank 9882 cfsmolem 10310 fin1a2lem5 10444 fin1a2lem6 10445 infm3 12227 wwlktovfo 14997 even2n 16379 smndex1mnd 18923 cycsubmel 19218 znf1o 21570 lmres 23308 ist1-2 23355 itg2monolem1 25785 lhop1lem 26052 elaa 26358 ulmcau 26438 reeff1o 26491 recosf1o 26577 chpo1ubb 27525 noetainflem4 27785 0reno 28429 istrkg2ld 28468 wlkswwlksf1o 29899 wwlksnextsurj 29920 nmopnegi 31984 nmop0 32005 nmfn0 32006 adjbd1o 32104 atom1d 32372 abfmpunirn 32662 rearchi 33374 eulerpartgbij 34374 eulerpartlemgh 34380 subfacp1lem3 35187 dfrdg2 35796 heiborlem7 37824 qsresid 38326 cxpi11d 42379 fimgmcyc 42544 eq0rabdioph 42787 elicores 45546 liminfpnfuz 45831 xlimpnfxnegmnf2 45873 fourierdlem70 46191 fourierdlem80 46201 ovolval3 46662 rexrsb 47112 |
| Copyright terms: Public domain | W3C validator |