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 2136, ax-11 2151, and ax-12 2167. (Revised by Steven Nguyen, 30-Apr-2023.) |
Ref | Expression |
---|---|
raleq | ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biidd 263 | . 2 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜑)) | |
2 | 1 | raleqbi1dv 3401 | 1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ∀wral 3135 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 df-clel 2890 df-ral 3140 |
This theorem is referenced by: raleqi 3411 raleqdv 3413 raleqbi1dvOLD 3415 sbralie 3469 r19.2zb 4437 inteq 4870 iineq1 4927 fri 5510 frsn 5632 fncnv 6420 isoeq4 7062 onminex 7511 tfinds 7563 f1oweALT 7662 frxp 7809 wfrlem1 7943 wfrlem15 7958 tfrlem1 8001 tfrlem12 8014 omeulem1 8197 ixpeq1 8460 undifixp 8486 ac6sfi 8750 frfi 8751 iunfi 8800 indexfi 8820 supeq1 8897 supeq2 8900 bnd2 9310 acneq 9457 aceq3lem 9534 dfac5lem4 9540 dfac8 9549 dfac9 9550 kmlem1 9564 kmlem10 9573 kmlem13 9576 cfval 9657 axcc2lem 9846 axcc4dom 9851 axdc3lem3 9862 axdc3lem4 9863 ac4c 9886 ac5 9887 ac6sg 9898 zorn2lem7 9912 xrsupsslem 12688 xrinfmsslem 12689 xrsupss 12690 xrinfmss 12691 fsuppmapnn0fiubex 13348 rexanuz 14693 rexfiuz 14695 modfsummod 15137 gcdcllem3 15838 lcmfval 15953 lcmf0val 15954 lcmfunsnlem 15973 coprmprod 15993 coprmproddvds 15995 isprs 17528 drsdirfi 17536 isdrs2 17537 ispos 17545 lubeldm 17579 lubval 17582 glbeldm 17592 glbval 17595 istos 17633 pospropd 17732 isdlat 17791 mhmpropd 17950 isghm 18296 cntzval 18389 efgval 18772 iscmn 18843 dfrhm2 19398 lidldvgen 19956 coe1fzgsumd 20398 evl1gsumd 20448 ocvval 20739 isobs 20792 mat0dimcrng 21007 mdetunilem9 21157 ist0 21856 cmpcovf 21927 is1stc 21977 2ndc1stc 21987 isref 22045 txflf 22542 ustuqtop4 22780 iscfilu 22824 ispsmet 22841 ismet 22860 isxmet 22861 cncfval 23423 lebnumlem3 23494 fmcfil 23802 iscfil3 23803 caucfil 23813 iscmet3 23823 cfilres 23826 minveclem3 23959 ovolfiniun 24029 finiunmbl 24072 volfiniun 24075 dvcn 24445 ulmval 24895 axtgcont1 26181 nb3grpr 27091 dfconngr1 27894 isconngr 27895 1conngr 27900 frgr0v 27968 isplig 28180 isgrpo 28201 isablo 28250 ocval 28984 acunirnmpt 30332 isomnd 30629 isorng 30799 prmidl 30876 ismbfm 31409 isanmbfm 31413 bnj865 32094 bnj1154 32168 bnj1296 32190 bnj1463 32224 derangval 32311 setinds 32920 dfon2lem3 32927 dfon2lem7 32931 tfisg 32952 poseq 32992 frrlem1 33020 frrlem13 33032 sltval2 33060 sltres 33066 nolesgn2o 33075 nodense 33093 nosupbnd2lem1 33112 brsslt 33151 dfrecs2 33308 dfrdg4 33309 isfne 33584 finixpnum 34758 mblfinlem1 34810 mbfresfi 34819 indexdom 34890 heibor1lem 34968 isexid2 35014 ismndo2 35033 rngomndo 35094 pridl 35196 smprngopr 35211 ispridlc 35229 setindtrs 39500 dford3lem2 39502 dfac11 39540 mnuop123d 40475 fnchoice 41163 axccdom 41363 axccd 41371 stoweidlem31 42193 stoweidlem57 42219 fourierdlem80 42348 fourierdlem103 42371 fourierdlem104 42372 isvonmbl 42797 paireqne 43550 requad2 43665 mgmhmpropd 43929 rnghmval 44090 zrrnghm 44116 bnd2d 44712 |
Copyright terms: Public domain | W3C validator |