| 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 3302 | 1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1541 ∀wral 3049 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-9 2123 ax-ext 2705 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1781 df-cleq 2725 df-ral 3050 df-rex 3059 |
| This theorem is referenced by: raleqOLD 3308 isoeq4 7263 frrlem1 8225 frrlem13 8237 smo11 8293 dffi2 9317 inficl 9319 dffi3 9325 dfom3 9547 aceq1 10018 dfac5lem4 10027 dfac5lem4OLD 10029 kmlem1 10052 kmlem10 10061 kmlem13 10064 kmlem14 10065 cofsmo 10170 infpssrlem4 10207 axdc3lem2 10352 elwina 10587 elina 10588 iswun 10605 eltskg 10651 elgrug 10693 elnp 10888 elnpi 10889 dfnn2 12148 dfnn3 12149 dfuzi 12574 coprmprod 16582 coprmproddvds 16584 ismri 17547 isprs 18212 isdrs 18217 ispos 18230 pospropd 18241 istos 18332 isdlat 18438 isipodrs 18453 mgmhmpropd 18616 issubmgm 18620 mhmpropd 18710 issubm 18721 subgacs 19083 nsgacs 19084 isghm 19137 isghmOLD 19138 ghmeql 19161 iscmn 19711 isomnd 20045 rnghmval 20368 dfrhm2 20402 zrrnghm 20461 isorng 20786 islss 20877 lssacs 20910 lmhmeql 20999 islbs 21020 lbsextlem1 21105 lbsextlem3 21107 lbsextlem4 21108 isobs 21667 mat0dimcrng 22395 istopg 22820 isbasisg 22872 basis2 22876 eltg2 22883 iscldtop 23020 neipeltop 23054 isreg 23257 regsep 23259 isnrm 23260 islly 23393 isnlly 23394 llyi 23399 nllyi 23400 islly2 23409 cldllycmp 23420 isfbas 23754 fbssfi 23762 isust 24129 elutop 24158 ustuqtop 24171 utopsnneip 24173 ispsmet 24229 ismet 24248 isxmet 24249 metrest 24449 cncfval 24818 fmcfil 25209 iscfil3 25210 caucfil 25220 iscmet3 25230 cfilres 25233 minveclem3 25366 wilthlem2 27016 wilthlem3 27017 wilth 27018 dfn0s2 28270 dfconngr1 30179 isconngr 30180 1conngr 30185 isplig 30467 isgrpo 30488 isablo 30537 disjabrex 32573 disjabrexf 32574 isrnsiga 34137 isldsys 34180 isros 34192 issros 34199 bnj1286 35042 bnj1452 35075 kur14lem9 35269 cvmscbv 35313 cvmsi 35320 cvmsval 35321 neibastop1 36414 neibastop2lem 36415 neibastop2 36416 rdgssun 37433 isbnd 37830 ismndo2 37924 rngomndo 37985 isidl 38064 ispsubsp 39854 sn-isghm 42781 isnacs 42811 mzpclval 42832 elmzpcl 42833 relpeq4 45054 permac8prim 45121 nelsubc3lem 49185 isthinc 49534 |
| Copyright terms: Public domain | W3C validator |