![]() |
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 | rexeqbidvv 3332 | 1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1542 ∃wrex 3071 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-cleq 2725 df-rex 3072 |
This theorem is referenced by: rexeqOLD 3337 friOLD 5633 frsn 5758 isofrlem 7324 f1oweALT 7946 frxp 8099 frxp2 8117 1sdomOLD 9237 oieq2 9495 zfregcl 9576 frmin 9731 hashge2el2difr 14429 cat1 18034 ishaus 22795 isreg 22805 isnrm 22808 lebnumlem3 24448 1vwmgr 29496 3vfriswmgr 29498 isgrpo 29715 pjhth 30611 bnj1154 33941 satfvsuc 34283 satf0suc 34298 sat1el2xp 34301 fmlasuc0 34306 isexid2 36629 ismndo2 36648 rngomndo 36709 stoweidlem28 44617 prprval 46055 |
Copyright terms: Public domain | W3C validator |