| 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 3319 | . 2 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 209 = wceq 1563 ∃wrex 3089 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-9 2155 ax-ext 2737 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-ex 1803 df-cleq 2757 df-rex 3090 |
| This theorem is referenced by: rexrab2 3666 rexprgf 4657 rextpg 4661 rexopabb 5502 rexxp 5818 elidinxpid 6037 elrid 6038 oarec 8535 brttrcl2 9671 ttrcltr 9673 rnttrcl 9679 wwlktovfo 14983 dvdsprmpweqnn 16933 4sqlem12 17004 pzriprnglem10 21597 pmatcollpw3fi1 22902 cmpfi 23522 txbas 23681 xkobval 23700 ustn0 24335 imasdsf1olem 24487 xpsdsval 24495 plyun0 26311 coeeu 26339 1cubr 26961 made0 28010 addsrid 28111 muls01 28259 mulsrid 28260 precsexlemcbv 28353 dfnbgr3 29593 wlkvtxedg 29898 wwlksn0 30117 eucrctshift 30499 adjbdln 32340 elunirnmbfm 34554 onvf1odlem2 35454 satfbrsuc 35724 fmla1 35745 satffunlem2lem2 35764 filnetlem4 36749 rexrabdioph 43378 fnwe2lem2 43635 fourierdlem70 46749 fourierdlem80 46759 dfclnbgr3 48447 stgr1 48582 |
| Copyright terms: Public domain | W3C validator |