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 2137, ax-11 2154, and ax-12 2171. (Revised by Steven Nguyen, 30-Apr-2023.) |
Ref | Expression |
---|---|
rexeq | ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biidd 261 | . 2 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜑)) | |
2 | 1 | rexeqbi1dv 3341 | 1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1539 ∃wrex 3065 |
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 1913 ax-6 1971 ax-7 2011 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 df-cleq 2730 df-ral 3069 df-rex 3070 |
This theorem is referenced by: rexeqi 3347 rexeqdv 3349 unieqOLD 4851 axrep6g 5217 exss 5378 qseq1 8552 pssnn 8951 1sdom 9025 pssnnOLD 9040 indexfi 9127 supeq1 9204 bnd2 9651 dfac2b 9886 cflem 10002 cflecard 10009 cfeq0 10012 cfsuc 10013 cfflb 10015 cofsmo 10025 elwina 10442 eltskg 10506 rankcf 10533 elnp 10743 elnpi 10744 genpv 10755 xrsupsslem 13041 xrinfmsslem 13042 xrsupss 13043 xrinfmss 13044 hashge2el2difr 14195 cat1 17812 isdrs 18019 isipodrs 18255 neifval 22250 ishaus 22473 2ndc1stc 22602 1stcrest 22604 lly1stc 22647 isref 22660 islocfin 22668 tx1stc 22801 isust 23355 iscfilu 23440 met1stc 23677 iscfil 24429 ishpg 27120 isgrpo 28859 chne0 29856 pstmfval 31846 dya2iocuni 32250 satfvsuc 33323 satf0suc 33338 sat1el2xp 33341 fmlasuc0 33346 noetasuplem4 33939 altxpeq1 34275 altxpeq2 34276 elhf2 34477 bj-sngleq 35157 cover2g 35873 indexdom 35892 istotbnd 35927 pmapglb2xN 37786 paddval 37812 elpadd0 37823 diophrex 40597 hbtlem1 40948 hbtlem7 40950 mnuop23d 41884 ismnushort 41919 sprval 44931 sprsymrelfvlem 44942 sprsymrelfv 44946 sprsymrelfo 44949 prprval 44966 |
Copyright terms: Public domain | W3C validator |