![]() |
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.) |
Ref | Expression |
---|---|
raleq | ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2793 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfcv 2793 | . 2 ⊢ Ⅎ𝑥𝐵 | |
3 | 1, 2 | raleqf 3164 | 1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1523 ∀wral 2941 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ral 2946 |
This theorem is referenced by: raleqi 3172 raleqdv 3174 raleqbi1dv 3176 sbralie 3214 r19.2zb 4094 inteq 4510 iineq1 4567 fri 5105 frsn 5223 fncnv 6000 isoeq4 6610 onminex 7049 tfinds 7101 f1oweALT 7194 frxp 7332 wfrlem1 7459 wfrlem15 7474 tfrlem1 7517 tfrlem12 7530 omeulem1 7707 ixpeq1 7961 undifixp 7986 ac6sfi 8245 frfi 8246 iunfi 8295 indexfi 8315 supeq1 8392 supeq2 8395 bnd2 8794 acneq 8904 aceq3lem 8981 dfac5lem4 8987 dfac8 8995 dfac9 8996 kmlem1 9010 kmlem10 9019 kmlem13 9022 cfval 9107 axcc2lem 9296 axcc4dom 9301 axdc3lem3 9312 axdc3lem4 9313 ac4c 9336 ac5 9337 ac6sg 9348 zorn2lem7 9362 xrsupsslem 12175 xrinfmsslem 12176 xrsupss 12177 xrinfmss 12178 fsuppmapnn0fiubex 12832 rexanuz 14129 rexfiuz 14131 modfsummod 14570 gcdcllem3 15270 lcmfval 15381 lcmf0val 15382 lcmfunsnlem 15401 coprmprod 15422 coprmproddvds 15424 isprs 16977 drsdirfi 16985 isdrs2 16986 ispos 16994 lubeldm 17028 lubval 17031 glbeldm 17041 glbval 17044 istos 17082 pospropd 17181 isdlat 17240 mhmpropd 17388 isghm 17707 cntzval 17800 efgval 18176 iscmn 18246 dfrhm2 18765 lidldvgen 19303 coe1fzgsumd 19720 evl1gsumd 19769 ocvval 20059 isobs 20112 mat0dimcrng 20324 mdetunilem9 20474 ist0 21172 cmpcovf 21242 is1stc 21292 2ndc1stc 21302 isref 21360 txflf 21857 ustuqtop4 22095 iscfilu 22139 ispsmet 22156 ismet 22175 isxmet 22176 cncfval 22738 lebnumlem3 22809 fmcfil 23116 iscfil3 23117 caucfil 23127 iscmet3 23137 cfilres 23140 minveclem3 23246 ovolfiniun 23315 finiunmbl 23358 volfiniun 23361 dvcn 23729 ulmval 24179 axtgcont1 25412 tgcgr4 25471 nb3grpr 26328 prcliscplgr 26365 dfconngr1 27166 isconngr 27167 1conngr 27172 frgr0v 27241 isplig 27458 isgrpo 27479 isablo 27528 ocval 28267 acunirnmpt 29587 isomnd 29829 isorng 29927 ismbfm 30442 isanmbfm 30446 bnj865 31119 bnj1154 31193 bnj1296 31215 bnj1463 31249 derangval 31275 setinds 31807 dfon2lem3 31814 dfon2lem7 31818 tfisg 31840 poseq 31878 frrlem1 31905 sltval2 31934 sltres 31940 nolesgn2o 31949 nodense 31967 nosupbnd2lem1 31986 brsslt 32025 dfrecs2 32182 dfrdg4 32183 isfne 32459 finixpnum 33524 mblfinlem1 33576 mbfresfi 33586 indexdom 33659 heibor1lem 33738 isexid2 33784 ismndo2 33803 rngomndo 33864 pridl 33966 smprngopr 33981 ispridlc 33999 setindtrs 37909 dford3lem2 37911 dfac11 37949 fnchoice 39502 axccdom 39730 axccd 39743 stoweidlem31 40566 stoweidlem57 40592 fourierdlem80 40721 fourierdlem103 40744 fourierdlem104 40745 isvonmbl 41173 mgmhmpropd 42110 rnghmval 42216 zrrnghm 42242 bnd2d 42753 |
Copyright terms: Public domain | W3C validator |