Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rexeq | Structured version Visualization version GIF version |
Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) Remove usage of ax-10 2144, ax-11 2161, and ax-12 2178. (Revised by Steven Nguyen, 30-Apr-2023.) |
Ref | Expression |
---|---|
rexeq | ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biidd 265 | . 2 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜑)) | |
2 | 1 | rexeqbi1dv 3308 | 1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 = wceq 1542 ∃wrex 3054 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-9 2123 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1787 df-cleq 2730 df-ral 3058 df-rex 3059 |
This theorem is referenced by: rexeqi 3314 rexeqdv 3316 unieqOLD 4805 exss 5318 qseq1 8367 pssnn 8760 1sdom 8793 pssnnOLD 8808 indexfi 8898 supeq1 8975 bnd2 9388 dfac2b 9623 cflem 9739 cflecard 9746 cfeq0 9749 cfsuc 9750 cfflb 9752 cofsmo 9762 elwina 10179 eltskg 10243 rankcf 10270 elnp 10480 elnpi 10481 genpv 10492 xrsupsslem 12776 xrinfmsslem 12777 xrsupss 12778 xrinfmss 12779 hashge2el2difr 13926 cat1 17462 isdrs 17653 isipodrs 17880 neifval 21843 ishaus 22066 2ndc1stc 22195 1stcrest 22197 lly1stc 22240 isref 22253 islocfin 22261 tx1stc 22394 isust 22948 iscfilu 23033 met1stc 23267 iscfil 24010 ishpg 26697 isgrpo 28424 chne0 29421 pstmfval 31410 dya2iocuni 31812 satfvsuc 32886 satf0suc 32901 sat1el2xp 32904 fmlasuc0 32909 noetasuplem4 33572 altxpeq1 33905 altxpeq2 33906 elhf2 34107 bj-sngleq 34769 cover2g 35485 indexdom 35504 istotbnd 35539 pmapglb2xN 37398 paddval 37424 elpadd0 37435 diophrex 40153 hbtlem1 40504 hbtlem7 40506 mnuop23d 41410 sprval 44449 sprsymrelfvlem 44460 sprsymrelfv 44464 sprsymrelfo 44467 prprval 44484 |
Copyright terms: Public domain | W3C validator |