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 3308 | 1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 = wceq 1543 ∀wral 3054 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-9 2120 ax-ext 2706 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-cleq 2726 df-ral 3059 |
This theorem is referenced by: raleq 3312 isoeq4 7118 frrlem1 8016 frrlem13 8028 wfrlem1 8043 wfrlem4 8047 wfrlem15 8058 smo11 8090 dffi2 9028 inficl 9030 dffi3 9036 dfom3 9251 aceq1 9714 dfac5lem4 9723 kmlem1 9747 kmlem10 9756 kmlem13 9759 kmlem14 9760 cofsmo 9866 infpssrlem4 9903 axdc3lem2 10048 elwina 10283 elina 10284 iswun 10301 eltskg 10347 elgrug 10389 elnp 10584 elnpi 10585 dfnn2 11826 dfnn3 11827 dfuzi 12251 coprmprod 16199 coprmproddvds 16201 ismri 17106 isprs 17776 isdrs 17780 ispos 17793 pospropd 17805 istos 17896 isdlat 18000 isipodrs 18015 mhmpropd 18196 issubm 18202 subgacs 18549 nsgacs 18550 isghm 18594 ghmeql 18617 iscmn 19150 dfrhm2 19709 islss 19943 lssacs 19976 lmhmeql 20064 islbs 20085 lbsextlem1 20167 lbsextlem3 20169 lbsextlem4 20170 isobs 20654 mat0dimcrng 21339 istopg 21764 isbasisg 21816 basis2 21820 eltg2 21827 iscldtop 21964 neipeltop 21998 isreg 22201 regsep 22203 isnrm 22204 islly 22337 isnlly 22338 llyi 22343 nllyi 22344 islly2 22353 cldllycmp 22364 isfbas 22698 fbssfi 22706 isust 23073 elutop 23103 ustuqtop 23116 utopsnneip 23118 ispsmet 23174 ismet 23193 isxmet 23194 metrest 23394 cncfval 23757 fmcfil 24141 iscfil3 24142 caucfil 24152 iscmet3 24162 cfilres 24165 minveclem3 24298 wilthlem2 25923 wilthlem3 25924 wilth 25925 dfconngr1 28243 isconngr 28244 1conngr 28249 isplig 28529 isgrpo 28550 isablo 28599 disjabrex 30612 disjabrexf 30613 isomnd 31018 isorng 31189 isrnsiga 31765 isldsys 31808 isros 31820 issros 31827 bnj1286 32684 bnj1452 32717 kur14lem9 32861 cvmscbv 32905 cvmsi 32912 cvmsval 32913 neibastop1 34242 neibastop2lem 34243 neibastop2 34244 rdgssun 35243 isbnd 35632 ismndo2 35726 rngomndo 35787 isidl 35866 ispsubsp 37453 isnacs 40181 mzpclval 40202 elmzpcl 40203 mgmhmpropd 44966 issubmgm 44970 rnghmval 45076 zrrnghm 45102 isthinc 45929 |
Copyright terms: Public domain | W3C validator |