![]() |
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 2130, ax-11 2147, and ax-12 2167. (Revised by Steven Nguyen, 30-Apr-2023.) Shorten other proofs. (Revised by Wolf Lammen, 8-Mar-2025.) |
Ref | Expression |
---|---|
raleq | ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexeq 3311 | . . 3 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∃𝑥 ∈ 𝐵 ¬ 𝜑)) | |
2 | rexnal 3090 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑) | |
3 | rexnal 3090 | . . 3 ⊢ (∃𝑥 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐵 𝜑) | |
4 | 1, 2, 3 | 3bitr3g 312 | . 2 ⊢ (𝐴 = 𝐵 → (¬ ∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐵 𝜑)) |
5 | 4 | con4bid 316 | 1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 = wceq 1534 ∀wral 3051 ∃wrex 3060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-cleq 2718 df-ral 3052 df-rex 3061 |
This theorem is referenced by: raleqi 3313 raleqdv 3315 sbralieALT 3343 r19.2zb 4490 inteq 4949 iineq1 5010 friOLD 5635 frsn 5761 fncnv 6624 isoeq4 7324 onminex 7803 tfisg 7856 tfinds 7862 f1oweALT 7978 frxp 8132 frxp2 8150 poseq 8164 frrlem1 8293 frrlem13 8305 wfrlem1OLD 8330 wfrlem15OLD 8345 tfrlem1 8398 tfrlem12 8411 omeulem1 8604 ixpeq1 8929 undifixp 8955 ac6sfi 9314 frfi 9315 iunfi 9378 indexfi 9397 supeq1 9481 supeq2 9484 brttrcl2 9750 ssttrcl 9751 ttrcltr 9752 bnd2 9929 acneq 10079 aceq3lem 10156 dfac5lem4 10162 dfac8 10171 dfac9 10172 kmlem1 10186 kmlem10 10195 kmlem13 10198 cfval 10281 axcc2lem 10470 axcc4dom 10475 axdc3lem3 10486 axdc3lem4 10487 ac4c 10510 ac5 10511 ac6sg 10522 zorn2lem7 10536 xrsupsslem 13334 xrinfmsslem 13335 xrsupss 13336 xrinfmss 13337 fsuppmapnn0fiubex 14006 rexanuz 15345 rexfiuz 15347 modfsummod 15793 gcdcllem3 16496 lcmfval 16617 lcmf0val 16618 lcmfunsnlem 16637 coprmprod 16657 coprmproddvds 16659 isprs 18317 drsdirfi 18325 isdrs2 18326 ispos 18334 pospropd 18347 lubeldm 18373 lubval 18376 glbeldm 18386 glbval 18389 istos 18438 isdlat 18542 mgmhmpropd 18686 mhmpropd 18777 isghm 19205 isghmOLD 19206 cntzval 19311 efgval 19711 iscmn 19783 rnghmval 20418 dfrhm2 20452 zrrnghm 20514 lidldvgen 21319 ocvval 21659 isobs 21714 coe1fzgsumd 22292 evl1gsumd 22345 mat0dimcrng 22460 mdetunilem9 22610 ist0 23312 cmpcovf 23383 is1stc 23433 2ndc1stc 23443 isref 23501 txflf 23998 ustuqtop4 24237 iscfilu 24281 ispsmet 24298 ismet 24317 isxmet 24318 cncfval 24896 lebnumlem3 24977 fmcfil 25288 iscfil3 25289 caucfil 25299 iscmet3 25309 cfilres 25312 minveclem3 25445 ovolfiniun 25518 finiunmbl 25561 volfiniun 25564 dvcn 25939 ulmval 26406 sltval2 27683 sltres 27689 nolesgn2o 27698 nogesgn1o 27700 nodense 27719 nosupbnd2lem1 27742 noinfbnd2lem1 27757 brsslt 27812 madebday 27920 negsprop 28041 mulsprop 28128 axtgcont1 28392 nb3grpr 29315 dfconngr1 30118 isconngr 30119 1conngr 30124 frgr0v 30192 isplig 30406 isgrpo 30427 isablo 30476 ocval 31210 acunirnmpt 32576 isomnd 32940 isorng 33182 prmidl 33321 ismbfm 34097 bnj865 34781 bnj1154 34857 bnj1296 34879 bnj1463 34913 wevgblacfn 34949 derangval 35008 setinds 35615 dfon2lem3 35622 dfon2lem7 35626 dfrecs2 35787 dfrdg4 35788 isfne 36064 finixpnum 37319 mblfinlem1 37371 mbfresfi 37380 indexdom 37448 heibor1lem 37523 isexid2 37569 ismndo2 37588 rngomndo 37649 pridl 37751 smprngopr 37766 ispridlc 37784 sn-isghm 42365 setindtrs 42720 dford3lem2 42722 dfac11 42760 rp-intrabeq 42923 rp-unirabeq 42924 rp-brsslt 43127 mnuop123d 43973 fnchoice 44665 axccdom 44865 axccd 44872 stoweidlem31 45688 stoweidlem57 45714 fourierdlem80 45843 fourierdlem103 45866 fourierdlem104 45867 isvonmbl 46295 paireqne 47119 requad2 47231 isthinc 48378 0thincg 48407 bnd2d 48463 |
Copyright terms: Public domain | W3C validator |