![]() |
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 3319 | 1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1534 ∀wral 3051 |
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: raleqOLD 3325 isoeq4 7332 frrlem1 8301 frrlem13 8313 wfrlem1OLD 8338 wfrlem4OLD 8342 wfrlem15OLD 8353 smo11 8394 dffi2 9466 inficl 9468 dffi3 9474 dfom3 9690 aceq1 10160 dfac5lem4 10169 kmlem1 10193 kmlem10 10202 kmlem13 10205 kmlem14 10206 cofsmo 10312 infpssrlem4 10349 axdc3lem2 10494 elwina 10729 elina 10730 iswun 10747 eltskg 10793 elgrug 10835 elnp 11030 elnpi 11031 dfnn2 12277 dfnn3 12278 dfuzi 12705 coprmprod 16662 coprmproddvds 16664 ismri 17644 isprs 18322 isdrs 18326 ispos 18339 pospropd 18352 istos 18443 isdlat 18547 isipodrs 18562 mgmhmpropd 18691 issubmgm 18695 mhmpropd 18782 issubm 18793 subgacs 19155 nsgacs 19156 isghm 19209 isghmOLD 19210 ghmeql 19233 iscmn 19787 rnghmval 20422 dfrhm2 20456 zrrnghm 20518 islss 20911 lssacs 20944 lmhmeql 21033 islbs 21054 lbsextlem1 21139 lbsextlem3 21141 lbsextlem4 21142 isobs 21718 mat0dimcrng 22463 istopg 22888 isbasisg 22941 basis2 22945 eltg2 22952 iscldtop 23090 neipeltop 23124 isreg 23327 regsep 23329 isnrm 23330 islly 23463 isnlly 23464 llyi 23469 nllyi 23470 islly2 23479 cldllycmp 23490 isfbas 23824 fbssfi 23832 isust 24199 elutop 24229 ustuqtop 24242 utopsnneip 24244 ispsmet 24301 ismet 24320 isxmet 24321 metrest 24524 cncfval 24899 fmcfil 25291 iscfil3 25292 caucfil 25302 iscmet3 25312 cfilres 25315 minveclem3 25448 wilthlem2 27097 wilthlem3 27098 wilth 27099 dfn0s2 28304 dfconngr1 30121 isconngr 30122 1conngr 30127 isplig 30409 isgrpo 30430 isablo 30479 disjabrex 32502 disjabrexf 32503 isomnd 32936 isorng 33177 isrnsiga 33946 isldsys 33989 isros 34001 issros 34008 bnj1286 34864 bnj1452 34897 kur14lem9 35042 cvmscbv 35086 cvmsi 35093 cvmsval 35094 neibastop1 36071 neibastop2lem 36072 neibastop2 36073 rdgssun 37085 isbnd 37481 ismndo2 37575 rngomndo 37636 isidl 37715 ispsubsp 39444 sn-isghm 42327 isnacs 42361 mzpclval 42382 elmzpcl 42383 isthinc 48342 |
Copyright terms: Public domain | W3C validator |