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.) |
Ref | Expression |
---|---|
raleqd.1 | ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
raleqbi1dv | ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | raleq 3115 | . 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) | |
2 | raleqd.1 | . . 3 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) | |
3 | 2 | ralbidv 2969 | . 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)) |
4 | 1, 3 | bitrd 267 | 1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 = wceq 1475 ∀wral 2896 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 |
This theorem is referenced by: isoeq4 6470 wfrlem1 7301 wfrlem4 7305 wfrlem15 7316 smo11 7348 dffi2 8212 inficl 8214 dffi3 8220 dfom3 8427 aceq1 8823 dfac5lem4 8832 kmlem1 8855 kmlem10 8864 kmlem13 8867 kmlem14 8868 cofsmo 8974 infpssrlem4 9011 axdc3lem2 9156 elwina 9387 elina 9388 iswun 9405 eltskg 9451 elgrug 9493 elnp 9688 elnpi 9689 dfnn2 10910 dfnn3 10911 dfuzi 11344 coprmprod 15213 coprmproddvds 15215 ismri 16114 isprs 16753 isdrs 16757 ispos 16770 istos 16858 pospropd 16957 isipodrs 16984 isdlat 17016 mhmpropd 17164 issubm 17170 subgacs 17452 nsgacs 17453 isghm 17483 ghmeql 17506 iscmn 18023 dfrhm2 18540 islss 18756 lssacs 18788 lmhmeql 18876 islbs 18897 lbsextlem1 18979 lbsextlem3 18981 lbsextlem4 18982 isobs 19883 mat0dimcrng 20095 istopg 20525 isbasisg 20562 basis2 20566 eltg2 20573 iscldtop 20709 neipeltop 20743 isreg 20946 regsep 20948 isnrm 20949 islly 21081 isnlly 21082 llyi 21087 nllyi 21088 islly2 21097 cldllycmp 21108 isfbas 21443 fbssfi 21451 isust 21817 elutop 21847 ustuqtop 21860 utopsnneip 21862 ispsmet 21919 ismet 21938 isxmet 21939 metrest 22139 cncfval 22499 fmcfil 22878 iscfil3 22879 caucfil 22889 iscmet3 22899 cfilres 22902 minveclem3 23008 wilthlem2 24595 wilthlem3 24596 wilth 24597 isfrgra 26517 isplig 26720 isgrpo 26735 isablo 26784 disjabrex 28777 disjabrexf 28778 isomnd 29032 isorng 29130 isrnsigaOLD 29502 isrnsiga 29503 isldsys 29546 isros 29558 issros 29565 bnj1286 30341 bnj1452 30374 kur14lem9 30450 cvmscbv 30494 cvmsi 30501 cvmsval 30502 frrlem1 31024 frrlem4 31027 neibastop1 31524 neibastop2lem 31525 neibastop2 31526 isbnd 32749 ismndo2 32843 rngomndo 32904 isidl 32983 ispsubsp 34049 isnacs 36285 mzpclval 36306 elmzpcl 36307 dfconngr1 41355 mgmhmpropd 41575 issubmgm 41579 rnghmval 41681 zrrnghm 41707 |
Copyright terms: Public domain | W3C validator |