![]() |
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 3334 | 1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 = wceq 1537 ∃wrex 3068 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-cleq 2727 df-rex 3069 |
This theorem is referenced by: rexeqOLD 3339 friOLD 5647 frsn 5776 isofrlem 7360 f1oweALT 7996 frxp 8150 frxp2 8168 1sdomOLD 9283 oieq2 9551 zfregcl 9632 frmin 9787 hashge2el2difr 14517 cat1 18151 ishaus 23346 isreg 23356 isnrm 23359 lebnumlem3 25009 1vwmgr 30305 3vfriswmgr 30307 isgrpo 30526 pjhth 31422 bnj1154 34992 satfvsuc 35346 satf0suc 35361 sat1el2xp 35364 fmlasuc0 35369 isexid2 37842 ismndo2 37861 rngomndo 37922 stoweidlem28 45984 prprval 47439 |
Copyright terms: Public domain | W3C validator |