| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > raleqbi1dv | Structured version Visualization version GIF version | ||
| Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) (Proof shortened by Steven Nguyen, 5-May-2023.) |
| Ref | Expression |
|---|---|
| raleqbi1dv.1 | ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| raleqbi1dv | ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id 22 | . 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵) | |
| 2 | raleqbi1dv.1 | . 2 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) | |
| 3 | 1, 2 | raleqbidvv 3334 | 1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∀wral 3061 |
| 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: raleqOLD 3340 isoeq4 7340 frrlem1 8311 frrlem13 8323 wfrlem1OLD 8348 wfrlem4OLD 8352 wfrlem15OLD 8363 smo11 8404 dffi2 9463 inficl 9465 dffi3 9471 dfom3 9687 aceq1 10157 dfac5lem4 10166 dfac5lem4OLD 10168 kmlem1 10191 kmlem10 10200 kmlem13 10203 kmlem14 10204 cofsmo 10309 infpssrlem4 10346 axdc3lem2 10491 elwina 10726 elina 10727 iswun 10744 eltskg 10790 elgrug 10832 elnp 11027 elnpi 11028 dfnn2 12279 dfnn3 12280 dfuzi 12709 coprmprod 16698 coprmproddvds 16700 ismri 17674 isprs 18342 isdrs 18347 ispos 18360 pospropd 18372 istos 18463 isdlat 18567 isipodrs 18582 mgmhmpropd 18711 issubmgm 18715 mhmpropd 18805 issubm 18816 subgacs 19179 nsgacs 19180 isghm 19233 isghmOLD 19234 ghmeql 19257 iscmn 19807 rnghmval 20440 dfrhm2 20474 zrrnghm 20536 islss 20932 lssacs 20965 lmhmeql 21054 islbs 21075 lbsextlem1 21160 lbsextlem3 21162 lbsextlem4 21163 isobs 21740 mat0dimcrng 22476 istopg 22901 isbasisg 22954 basis2 22958 eltg2 22965 iscldtop 23103 neipeltop 23137 isreg 23340 regsep 23342 isnrm 23343 islly 23476 isnlly 23477 llyi 23482 nllyi 23483 islly2 23492 cldllycmp 23503 isfbas 23837 fbssfi 23845 isust 24212 elutop 24242 ustuqtop 24255 utopsnneip 24257 ispsmet 24314 ismet 24333 isxmet 24334 metrest 24537 cncfval 24914 fmcfil 25306 iscfil3 25307 caucfil 25317 iscmet3 25327 cfilres 25330 minveclem3 25463 wilthlem2 27112 wilthlem3 27113 wilth 27114 dfn0s2 28336 dfconngr1 30207 isconngr 30208 1conngr 30213 isplig 30495 isgrpo 30516 isablo 30565 disjabrex 32595 disjabrexf 32596 isomnd 33078 isorng 33329 isrnsiga 34114 isldsys 34157 isros 34169 issros 34176 bnj1286 35033 bnj1452 35066 kur14lem9 35219 cvmscbv 35263 cvmsi 35270 cvmsval 35271 neibastop1 36360 neibastop2lem 36361 neibastop2 36362 rdgssun 37379 isbnd 37787 ismndo2 37881 rngomndo 37942 isidl 38021 ispsubsp 39747 sn-isghm 42683 isnacs 42715 mzpclval 42736 elmzpcl 42737 relpeq4 44968 isthinc 49069 |
| Copyright terms: Public domain | W3C validator |