![]() |
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 2079, ax-11 2093, and ax-12 2106. (Revised by Steven Nguyen, 30-Apr-2023.) |
Ref | Expression |
---|---|
raleq | ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biidd 254 | . 2 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜑)) | |
2 | 1 | raleqbi1dv 3337 | 1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1507 ∀wral 3082 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-ext 2744 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-cleq 2765 df-clel 2840 df-ral 3087 |
This theorem is referenced by: raleqi 3347 raleqdv 3349 raleqbi1dvOLD 3351 sbralie 3391 r19.2zb 4318 inteq 4748 iineq1 4804 fri 5365 frsn 5485 fncnv 6257 isoeq4 6894 onminex 7336 tfinds 7388 f1oweALT 7483 frxp 7623 wfrlem1 7755 wfrlem15 7771 tfrlem1 7814 tfrlem12 7827 omeulem1 8007 ixpeq1 8268 undifixp 8293 ac6sfi 8555 frfi 8556 iunfi 8605 indexfi 8625 supeq1 8702 supeq2 8705 bnd2 9114 acneq 9261 aceq3lem 9338 dfac5lem4 9344 dfac8 9353 dfac9 9354 kmlem1 9368 kmlem10 9377 kmlem13 9380 cfval 9465 axcc2lem 9654 axcc4dom 9659 axdc3lem3 9670 axdc3lem4 9671 ac4c 9694 ac5 9695 ac6sg 9706 zorn2lem7 9720 xrsupsslem 12514 xrinfmsslem 12515 xrsupss 12516 xrinfmss 12517 fsuppmapnn0fiubex 13173 rexanuz 14564 rexfiuz 14566 modfsummod 15007 gcdcllem3 15708 lcmfval 15819 lcmf0val 15820 lcmfunsnlem 15839 coprmprod 15859 coprmproddvds 15861 isprs 17410 drsdirfi 17418 isdrs2 17419 ispos 17427 lubeldm 17461 lubval 17464 glbeldm 17474 glbval 17477 istos 17515 pospropd 17614 isdlat 17673 mhmpropd 17821 isghm 18141 cntzval 18234 efgval 18613 iscmn 18685 dfrhm2 19204 lidldvgen 19761 coe1fzgsumd 20185 evl1gsumd 20234 ocvval 20525 isobs 20578 mat0dimcrng 20795 mdetunilem9 20945 ist0 21644 cmpcovf 21715 is1stc 21765 2ndc1stc 21775 isref 21833 txflf 22330 ustuqtop4 22568 iscfilu 22612 ispsmet 22629 ismet 22648 isxmet 22649 cncfval 23211 lebnumlem3 23282 fmcfil 23590 iscfil3 23591 caucfil 23601 iscmet3 23611 cfilres 23614 minveclem3 23747 ovolfiniun 23817 finiunmbl 23860 volfiniun 23863 dvcn 24233 ulmval 24683 axtgcont1 25968 tgcgr4 26031 nb3grpr 26879 dfconngr1 27729 isconngr 27730 1conngr 27735 frgr0v 27807 isplig 28042 isgrpo 28063 isablo 28112 ocval 28850 acunirnmpt 30180 isomnd 30443 isorng 30580 ismbfm 31184 isanmbfm 31188 bnj865 31871 bnj1154 31945 bnj1296 31967 bnj1463 32001 derangval 32028 setinds 32572 dfon2lem3 32579 dfon2lem7 32583 tfisg 32605 poseq 32645 frrlem1 32673 frrlem13 32685 sltval2 32713 sltres 32719 nolesgn2o 32728 nodense 32746 nosupbnd2lem1 32765 brsslt 32804 dfrecs2 32961 dfrdg4 32962 isfne 33237 finixpnum 34347 mblfinlem1 34399 mbfresfi 34408 indexdom 34480 heibor1lem 34558 isexid2 34604 ismndo2 34623 rngomndo 34684 pridl 34786 smprngopr 34801 ispridlc 34819 setindtrs 39047 dford3lem2 39049 dfac11 39087 mnuop123d 40002 fnchoice 40734 axccdom 40938 axccd 40947 stoweidlem31 41772 stoweidlem57 41798 fourierdlem80 41927 fourierdlem103 41950 fourierdlem104 41951 isvonmbl 42376 paireqne 43066 requad2 43181 mgmhmpropd 43445 rnghmval 43551 zrrnghm 43577 bnd2d 44176 |
Copyright terms: Public domain | W3C validator |