![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > raleqbidv | Structured version Visualization version GIF version |
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2079, ax-11 2093, and ax-12 2106 and reduce distinct variable conditions. (Revised by Steven Nguyen, 30-Apr-2023.) |
Ref | Expression |
---|---|
raleqbidv.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
raleqbidv.2 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
raleqbidv | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | raleqbidv.1 | . . . 4 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | 1 | eleq2d 2851 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
3 | raleqbidv.2 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 2, 3 | imbi12d 337 | . 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒))) |
5 | 4 | ralbidv2 3145 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1507 ∈ wcel 2050 ∀wral 3088 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-ext 2750 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-cleq 2771 df-clel 2846 df-ral 3093 |
This theorem is referenced by: raleqbi1dv 3343 f12dfv 6857 f13dfv 6858 knatar 6935 ofrfval 7237 fmpox 7575 ovmptss 7598 marypha1lem 8694 supeq123d 8711 oieq1 8773 acneq 9265 isfin1a 9514 fpwwe2cbv 9852 fpwwe2lem2 9854 fpwwecbv 9866 fpwwelem 9867 eltskg 9972 elgrug 10014 cau3lem 14578 rlim 14716 ello1 14736 elo1 14747 caurcvg2 14898 caucvgb 14900 fsum2dlem 14988 fsumcom2 14992 fprod2dlem 15197 fprodcom2 15201 pcfac 16094 vdwpc 16175 rami 16210 prmgaplem7 16252 prdsval 16587 ismre 16722 isacs2 16785 acsfiel 16786 iscat 16804 iscatd 16805 catidex 16806 catideu 16807 cidfval 16808 cidval 16809 catlid 16815 catrid 16816 comfeq 16837 catpropd 16840 monfval 16863 issubc 16966 fullsubc 16981 isfunc 16995 funcpropd 17031 isfull 17041 isfth 17045 fthpropd 17052 natfval 17077 initoval 17118 termoval 17119 isposd 17426 lubfval 17449 glbfval 17462 ismgm 17714 issstrmgm 17723 grpidval 17731 gsumvalx 17741 gsumpropd 17743 gsumress 17747 issgrp 17756 ismnddef 17767 ismndd 17784 mndpropd 17787 ismhm 17808 resmhm 17830 isgrp 17900 grppropd 17909 isgrpd2e 17913 isnsg 18095 nmznsg 18110 isghm 18132 isga 18195 subgga 18204 gsmsymgrfix 18320 gsmsymgreq 18324 gexval 18467 ispgp 18481 isslw 18497 sylow2blem2 18510 efgval 18604 efgi 18606 efgsdm 18617 cmnpropd 18678 iscmnd 18681 submcmn2 18720 gsumzaddlem 18797 dmdprd 18873 dprdcntz 18883 issrg 18983 isring 19027 ringpropd 19058 isirred 19175 sdrgacs 19305 abvfval 19314 abvpropd 19338 islmod 19363 islmodd 19365 lmodprop2d 19421 lssset 19430 islmhm 19524 reslmhm 19549 lmhmpropd 19570 islbs 19573 rrgval 19784 isdomn 19791 isassa 19812 isassad 19820 assapropd 19824 ltbval 19968 opsrval 19971 psgndiflemA 20450 isphl 20477 islindf 20661 islindf2 20663 lsslindf 20679 dmatval 20808 dmatcrng 20818 scmatcrng 20837 cpmat 21024 istopg 21210 restbas 21473 ordtrest2 21519 cnfval 21548 cnpfval 21549 ist0 21635 ist1 21636 ishaus 21637 iscnrm 21638 isnrm 21650 ist0-2 21659 ishaus2 21666 nrmsep3 21670 iscmp 21703 is1stc 21756 isptfin 21831 islocfin 21832 kgenval 21850 kgencn2 21872 txbas 21882 ptval 21885 dfac14 21933 isfil 22162 isufil 22218 isufl 22228 flfcntr 22358 ucnval 22592 iscusp 22614 prdsxmslem2 22845 tngngp3 22971 isnlm 22990 nmofval 23029 lebnumii 23276 iscau4 23588 iscmet 23593 iscmet3lem1 23600 iscmet3 23602 equivcmet 23626 ulmcaulem 24688 ulmcau 24689 fsumdvdscom 25467 dchrisumlem3 25772 pntibndlem2 25872 pntibnd 25874 pntlemp 25891 ostth2lem2 25915 trgcgrg 26006 tgcgr4 26022 isismt 26025 nbgr2vtx1edg 26838 nbuhgr2vtx1edgb 26840 uvtxval 26875 uvtxel 26876 uvtxel1 26884 uvtxusgrel 26891 cusgredg 26912 cplgr3v 26923 cplgrop 26925 usgredgsscusgredg 26947 isrgr 27047 isewlk 27090 iswlk 27098 iswwlks 27325 wlkiswwlks2 27364 isclwwlk 27493 clwlkclwwlklem1 27508 isconngr 27721 isconngr1 27722 isfrgr 27795 rspc2vd 27802 frgr1v 27808 nfrgr2v 27809 frgr3v 27812 1vwmgr 27813 3vfriswmgr 27815 3cyclfrgrrn1 27822 n4cyclfrgr 27828 isplig 28033 gidval 28069 vciOLD 28118 isvclem 28134 isnvlem 28167 lnoval 28309 ajfval 28366 isphg 28374 minvecolem3 28434 htth 28477 ressprs 30374 isslmd 30496 resv1r 30589 iscref 30752 ordtrest2NEW 30810 fmcncfil 30818 issiga 31015 isrnsigaOLD 31016 isrnsiga 31017 isldsys 31060 ismeas 31103 carsgval 31206 issibf 31236 sitgfval 31244 signstfvneq0 31489 istrkg2d 31585 ispconn 32055 issconn 32058 txpconn 32064 cvxpconn 32074 cvmscbv 32090 iscvm 32091 cvmsdisj 32102 cvmsss2 32106 snmlval 32163 elmrsubrn 32287 ismfs 32316 mclsval 32330 frrlem4 32647 fwddifnval 33145 bj-ismoore 33907 pibp19 34136 pibp21 34137 poimirlem28 34361 cover2g 34432 seqpo 34464 incsequz2 34466 caushft 34478 ismtyval 34520 isass 34566 isexid 34567 elghomlem1OLD 34605 isrngo 34617 isrngod 34618 isgrpda 34675 rngohomval 34684 iscom2 34715 idlval 34733 pridlval 34753 maxidlval 34759 elrefrels3 35203 elcnvrefrels3 35216 eleqvrels3 35273 lflset 35640 islfld 35643 isopos 35761 isoml 35819 isatl 35880 iscvlat 35904 ishlat1 35933 psubspset 36325 lautset 36663 pautsetN 36679 ldilfset 36689 ltrnfset 36698 dilfsetN 36733 trnfsetN 36736 trnsetN 36737 trlfset 36741 tendofset 37339 tendoset 37340 dihffval 37811 lpolsetN 38063 hdmapfval 38408 hgmapfval 38467 aomclem8 39057 islnm 39073 clsk1independent 39759 gneispace2 39845 gneispaceel2 39857 gneispacess2 39859 ioodvbdlimc1lem1 41647 ioodvbdlimc1lem2 41648 ioodvbdlimc2lem 41650 issal 42031 ismea 42165 isome 42208 iccpartiltu 42955 iccelpart 42966 isomgr 43357 isupwlk 43380 mgmpropd 43411 ismgmd 43412 ismgmhm 43419 resmgmhm 43434 iscllaw 43461 iscomlaw 43462 isasslaw 43464 isrng 43512 c0snmgmhm 43550 zlidlring 43564 uzlidlring 43565 dmatALTval 43823 islininds 43869 lindslinindsimp2 43886 ldepsnlinc 43931 elbigo 43980 |
Copyright terms: Public domain | W3C validator |