| 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 2141, ax-11 2157, and ax-12 2177. (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 3322 | . . 3 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∃𝑥 ∈ 𝐵 ¬ 𝜑)) | |
| 2 | rexnal 3100 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑) | |
| 3 | rexnal 3100 | . . 3 ⊢ (∃𝑥 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐵 𝜑) | |
| 4 | 1, 2, 3 | 3bitr3g 313 | . 2 ⊢ (𝐴 = 𝐵 → (¬ ∀𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐵 𝜑)) |
| 5 | 4 | con4bid 317 | 1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 = wceq 1540 ∀wral 3061 ∃wrex 3070 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-ral 3062 df-rex 3071 |
| This theorem is referenced by: raleqi 3324 raleqdv 3326 raleleq 3342 sbralieALT 3359 r19.2zb 4496 inteq 4949 iineq1 5009 friOLD 5643 frsn 5773 fncnv 6639 isoeq4 7340 onminex 7822 tfisg 7875 tfinds 7881 f1oweALT 7997 frxp 8151 frxp2 8169 poseq 8183 frrlem1 8311 frrlem13 8323 wfrlem1OLD 8348 wfrlem15OLD 8363 tfrlem1 8416 tfrlem12 8429 omeulem1 8620 ixpeq1 8948 undifixp 8974 ac6sfi 9320 frfi 9321 iunfi 9383 indexfi 9400 supeq1 9485 supeq2 9488 brttrcl2 9754 ssttrcl 9755 ttrcltr 9756 bnd2 9933 acneq 10083 aceq3lem 10160 dfac5lem4 10166 dfac5lem4OLD 10168 dfac8 10176 dfac9 10177 kmlem1 10191 kmlem10 10200 kmlem13 10203 cfval 10287 axcc2lem 10476 axcc4dom 10481 axdc3lem3 10492 axdc3lem4 10493 ac4c 10516 ac5 10517 ac6sg 10528 zorn2lem7 10542 xrsupsslem 13349 xrinfmsslem 13350 xrsupss 13351 xrinfmss 13352 fsuppmapnn0fiubex 14033 rexanuz 15384 rexfiuz 15386 modfsummod 15830 gcdcllem3 16538 lcmfval 16658 lcmf0val 16659 lcmfunsnlem 16678 coprmprod 16698 coprmproddvds 16700 isprs 18342 drsdirfi 18351 isdrs2 18352 ispos 18360 pospropd 18372 lubeldm 18398 lubval 18401 glbeldm 18411 glbval 18414 istos 18463 isdlat 18567 mgmhmpropd 18711 mhmpropd 18805 isghm 19233 isghmOLD 19234 cntzval 19339 efgval 19735 iscmn 19807 rnghmval 20440 dfrhm2 20474 zrrnghm 20536 lidldvgen 21344 ocvval 21685 isobs 21740 coe1fzgsumd 22308 evl1gsumd 22361 mat0dimcrng 22476 mdetunilem9 22626 ist0 23328 cmpcovf 23399 is1stc 23449 2ndc1stc 23459 isref 23517 txflf 24014 ustuqtop4 24253 iscfilu 24297 ispsmet 24314 ismet 24333 isxmet 24334 cncfval 24914 lebnumlem3 24995 fmcfil 25306 iscfil3 25307 caucfil 25317 iscmet3 25327 cfilres 25330 minveclem3 25463 ovolfiniun 25536 finiunmbl 25579 volfiniun 25582 dvcn 25957 ulmval 26423 sltval2 27701 sltres 27707 nolesgn2o 27716 nogesgn1o 27718 nodense 27737 nosupbnd2lem1 27760 noinfbnd2lem1 27775 brsslt 27830 madebday 27938 negsprop 28067 mulsprop 28156 axtgcont1 28476 nb3grpr 29399 dfconngr1 30207 isconngr 30208 1conngr 30213 frgr0v 30281 isplig 30495 isgrpo 30516 isablo 30565 ocval 31299 acunirnmpt 32669 isomnd 33078 isorng 33329 prmidl 33468 ismbfm 34252 bnj865 34937 bnj1154 35013 bnj1296 35035 bnj1463 35069 wevgblacfn 35114 derangval 35172 setinds 35779 dfon2lem3 35786 dfon2lem7 35790 dfrecs2 35951 dfrdg4 35952 isfne 36340 finixpnum 37612 mblfinlem1 37664 mbfresfi 37673 indexdom 37741 heibor1lem 37816 isexid2 37862 ismndo2 37881 rngomndo 37942 pridl 38044 smprngopr 38059 ispridlc 38077 sn-isghm 42683 setindtrs 43037 dford3lem2 43039 dfac11 43074 rp-intrabeq 43233 rp-unirabeq 43234 rp-brsslt 43436 mnuop123d 44281 relpeq4 44968 trfr 44979 fnchoice 45034 axccdom 45227 axccd 45234 stoweidlem31 46046 stoweidlem57 46072 fourierdlem80 46201 fourierdlem103 46224 fourierdlem104 46225 isvonmbl 46653 paireqne 47498 requad2 47610 isthinc 49069 0thincg 49107 bnd2d 49200 |
| Copyright terms: Public domain | W3C validator |