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 3116 | . 2 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)) | |
2 | raleqd.1 | . . 3 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) | |
3 | 2 | rexbidv 3034 | . 2 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓)) |
4 | 1, 3 | bitrd 267 | 1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 = wceq 1475 ∃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 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rex 2902 |
This theorem is referenced by: fri 5000 frsn 5112 isofrlem 6490 f1oweALT 7043 frxp 7174 1sdom 8048 oieq2 8301 zfregcl 8382 zfregclOLD 8384 ishaus 20936 isreg 20946 isnrm 20949 lebnumlem3 22570 1vwmgra 26530 3vfriswmgra 26532 isgrpo 26735 pjhth 27636 bnj1154 30321 frmin 30983 isexid2 32824 ismndo2 32843 rngomndo 32904 stoweidlem28 38921 1vwmgr 41446 3vfriswmgr 41448 |
Copyright terms: Public domain | W3C validator |