![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > raleq | Structured version Visualization version GIF version |
Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2137, ax-11 2154, and ax-12 2171. (Revised by Steven Nguyen, 30-Apr-2023.) |
Ref | Expression |
---|---|
raleq | ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biidd 261 | . 2 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜑)) | |
2 | 1 | raleqbi1dv 3305 | 1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1541 ∀wral 3062 |
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 2708 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-cleq 2729 df-ral 3063 |
This theorem is referenced by: raleqi 3309 raleqdv 3311 sbralie 3330 r19.2zb 4451 inteq 4908 iineq1 4969 friOLD 5592 frsn 5717 fncnv 6571 isoeq4 7261 onminex 7729 tfisg 7782 tfinds 7788 f1oweALT 7897 frxp 8050 frxp2 8068 poseq 8082 frrlem1 8209 frrlem13 8221 wfrlem1OLD 8246 wfrlem15OLD 8261 tfrlem1 8314 tfrlem12 8327 omeulem1 8521 ixpeq1 8804 undifixp 8830 ac6sfi 9189 frfi 9190 iunfi 9242 indexfi 9262 supeq1 9339 supeq2 9342 brttrcl2 9608 ssttrcl 9609 ttrcltr 9610 bnd2 9787 acneq 9937 aceq3lem 10014 dfac5lem4 10020 dfac8 10029 dfac9 10030 kmlem1 10044 kmlem10 10053 kmlem13 10056 cfval 10141 axcc2lem 10330 axcc4dom 10335 axdc3lem3 10346 axdc3lem4 10347 ac4c 10370 ac5 10371 ac6sg 10382 zorn2lem7 10396 xrsupsslem 13180 xrinfmsslem 13181 xrsupss 13182 xrinfmss 13183 fsuppmapnn0fiubex 13851 rexanuz 15190 rexfiuz 15192 modfsummod 15639 gcdcllem3 16341 lcmfval 16457 lcmf0val 16458 lcmfunsnlem 16477 coprmprod 16497 coprmproddvds 16499 isprs 18146 drsdirfi 18154 isdrs2 18155 ispos 18163 pospropd 18176 lubeldm 18202 lubval 18205 glbeldm 18215 glbval 18218 istos 18267 isdlat 18371 mhmpropd 18568 isghm 18967 cntzval 19060 efgval 19458 iscmn 19530 dfrhm2 20101 lidldvgen 20678 ocvval 21024 isobs 21079 coe1fzgsumd 21625 evl1gsumd 21675 mat0dimcrng 21771 mdetunilem9 21921 ist0 22623 cmpcovf 22694 is1stc 22744 2ndc1stc 22754 isref 22812 txflf 23309 ustuqtop4 23548 iscfilu 23592 ispsmet 23609 ismet 23628 isxmet 23629 cncfval 24203 lebnumlem3 24278 fmcfil 24588 iscfil3 24589 caucfil 24599 iscmet3 24609 cfilres 24612 minveclem3 24745 ovolfiniun 24817 finiunmbl 24860 volfiniun 24863 dvcn 25237 ulmval 25691 sltval2 26956 sltres 26962 nolesgn2o 26971 nogesgn1o 26973 nodense 26992 nosupbnd2lem1 27015 noinfbnd2lem1 27030 brsslt 27077 madebday 27178 axtgcont1 27239 nb3grpr 28159 dfconngr1 28961 isconngr 28962 1conngr 28967 frgr0v 29035 isplig 29247 isgrpo 29268 isablo 29317 ocval 30051 acunirnmpt 31404 isomnd 31735 isorng 31920 prmidl 32034 ismbfm 32662 bnj865 33347 bnj1154 33423 bnj1296 33445 bnj1463 33479 derangval 33573 setinds 34169 dfon2lem3 34176 dfon2lem7 34180 negsprop 34328 dfrecs2 34473 dfrdg4 34474 isfne 34749 finixpnum 36001 mblfinlem1 36053 mbfresfi 36062 indexdom 36131 heibor1lem 36206 isexid2 36252 ismndo2 36271 rngomndo 36332 pridl 36434 smprngopr 36449 ispridlc 36467 setindtrs 41258 dford3lem2 41260 dfac11 41298 rp-intrabeq 41464 rp-unirabeq 41465 rp-brsslt 41606 mnuop123d 42453 fnchoice 43145 axccdom 43348 axccd 43355 stoweidlem31 44173 stoweidlem57 44199 fourierdlem80 44328 fourierdlem103 44351 fourierdlem104 44352 isvonmbl 44780 paireqne 45604 requad2 45716 mgmhmpropd 45980 rnghmval 46090 zrrnghm 46116 isthinc 46942 0thincg 46971 bnd2d 47027 |
Copyright terms: Public domain | W3C validator |