![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexeqi | Structured version Visualization version GIF version |
Description: Equality inference for restricted existential quantifier. (Contributed by Mario Carneiro, 23-Apr-2015.) |
Ref | Expression |
---|---|
raleq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
rexeqi | ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | raleq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | rexeq 3320 | . 2 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1541 ∃wrex 3069 |
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 1913 ax-6 1971 ax-7 2011 ax-9 2116 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-cleq 2723 df-rex 3070 |
This theorem is referenced by: rexrab2 3692 rexprgf 4690 rextpg 4696 rexopabb 5521 rexxp 5834 elidinxpid 6034 elrid 6035 oarec 8545 brttrcl2 9691 ttrcltr 9693 rnttrcl 9699 wwlktovfo 14891 dvdsprmpweqnn 16800 4sqlem12 16871 pmatcollpw3fi1 22219 cmpfi 22841 txbas 23000 xkobval 23019 ustn0 23654 imasdsf1olem 23808 xpsdsval 23816 plyun0 25640 coeeu 25668 1cubr 26274 made0 27291 addsrid 27364 muls01 27482 mulsrid 27483 dfnbgr3 28460 wlkvtxedg 28766 wwlksn0 28982 eucrctshift 29361 adjbdln 31199 elunirnmbfm 33081 satfbrsuc 34188 fmla1 34209 satffunlem2lem2 34228 filnetlem4 35070 rexrabdioph 41303 fnwe2lem2 41564 fourierdlem70 44665 fourierdlem80 44675 |
Copyright terms: Public domain | W3C validator |