![]() |
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.) (Proof shortened by Steven Nguyen, 5-May-2023.) |
Ref | Expression |
---|---|
raleqbi1dv.1 | ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
rexeqbi1dv | ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵) | |
2 | raleqbi1dv.1 | . 2 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | rexeqbidv 3355 | 1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 = wceq 1538 ∃wrex 3107 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-cleq 2791 df-clel 2870 df-rex 3112 |
This theorem is referenced by: rexeq 3359 fri 5481 frsn 5603 isofrlem 7072 f1oweALT 7655 frxp 7803 1sdom 8705 oieq2 8961 zfregcl 9042 hashge2el2difr 13835 ishaus 21927 isreg 21937 isnrm 21940 lebnumlem3 23568 1vwmgr 28061 3vfriswmgr 28063 isgrpo 28280 pjhth 29176 bnj1154 32381 satfvsuc 32721 satf0suc 32736 sat1el2xp 32739 fmlasuc0 32744 frmin 33197 isexid2 35293 ismndo2 35312 rngomndo 35373 stoweidlem28 42670 prprval 44031 |
Copyright terms: Public domain | W3C validator |