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 | raleqbidv 3399 | 1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ∀wral 3135 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 df-clel 2890 df-ral 3140 |
This theorem is referenced by: raleq 3403 isoeq4 7062 wfrlem1 7943 wfrlem4 7947 wfrlem15 7958 smo11 7990 dffi2 8875 inficl 8877 dffi3 8883 dfom3 9098 aceq1 9531 dfac5lem4 9540 kmlem1 9564 kmlem10 9573 kmlem13 9576 kmlem14 9577 cofsmo 9679 infpssrlem4 9716 axdc3lem2 9861 elwina 10096 elina 10097 iswun 10114 eltskg 10160 elgrug 10202 elnp 10397 elnpi 10398 dfnn2 11639 dfnn3 11640 dfuzi 12061 coprmprod 15993 coprmproddvds 15995 ismri 16890 isprs 17528 isdrs 17532 ispos 17545 istos 17633 pospropd 17732 isipodrs 17759 isdlat 17791 mhmpropd 17950 issubm 17956 subgacs 18251 nsgacs 18252 isghm 18296 ghmeql 18319 iscmn 18843 dfrhm2 19398 islss 19635 lssacs 19668 lmhmeql 19756 islbs 19777 lbsextlem1 19859 lbsextlem3 19861 lbsextlem4 19862 isobs 20792 mat0dimcrng 21007 istopg 21431 isbasisg 21483 basis2 21487 eltg2 21494 iscldtop 21631 neipeltop 21665 isreg 21868 regsep 21870 isnrm 21871 islly 22004 isnlly 22005 llyi 22010 nllyi 22011 islly2 22020 cldllycmp 22031 isfbas 22365 fbssfi 22373 isust 22739 elutop 22769 ustuqtop 22782 utopsnneip 22784 ispsmet 22841 ismet 22860 isxmet 22861 metrest 23061 cncfval 23423 fmcfil 23802 iscfil3 23803 caucfil 23813 iscmet3 23823 cfilres 23826 minveclem3 23959 wilthlem2 25573 wilthlem3 25574 wilth 25575 dfconngr1 27894 isconngr 27895 1conngr 27900 isplig 28180 isgrpo 28201 isablo 28250 disjabrex 30260 disjabrexf 30261 isomnd 30629 isorng 30799 isrnsiga 31271 isldsys 31314 isros 31326 issros 31333 bnj1286 32188 bnj1452 32221 kur14lem9 32358 cvmscbv 32402 cvmsi 32409 cvmsval 32410 frrlem1 33020 frrlem13 33032 neibastop1 33604 neibastop2lem 33605 neibastop2 33606 rdgssun 34541 isbnd 34939 ismndo2 35033 rngomndo 35094 isidl 35173 ispsubsp 36761 isnacs 39179 mzpclval 39200 elmzpcl 39201 mgmhmpropd 43929 issubmgm 43933 rnghmval 44090 zrrnghm 44116 |
Copyright terms: Public domain | W3C validator |