Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rexeqbi1dv | Structured version Visualization version GIF version |
Description: Equality deduction for restricted existential quantifier. (Contributed by NM, 18-Mar-1997.) |
Ref | Expression |
---|---|
raleqd.1 | ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
rexeqbi1dv | ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexeq 3139 | . 2 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)) | |
2 | raleqd.1 | . . 3 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) | |
3 | 2 | rexbidv 3052 | . 2 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓)) |
4 | 1, 3 | bitrd 268 | 1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1483 ∃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 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rex 2918 |
This theorem is referenced by: fri 5076 frsn 5189 isofrlem 6590 f1oweALT 7152 frxp 7287 1sdom 8163 oieq2 8418 zfregcl 8499 zfregclOLD 8501 ishaus 21126 isreg 21136 isnrm 21139 lebnumlem3 22762 1vwmgr 27140 3vfriswmgr 27142 isgrpo 27351 pjhth 28252 bnj1154 31067 frmin 31739 isexid2 33654 ismndo2 33673 rngomndo 33734 stoweidlem28 40245 |
Copyright terms: Public domain | W3C validator |