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 2136, ax-11 2151, and ax-12 2167 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 2895 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
3 | raleqbidv.2 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 2, 3 | imbi12d 346 | . 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒))) |
5 | 4 | ralbidv2 3192 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ∈ wcel 2105 ∀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: raleqbi1dv 3401 rspc2vd 3929 f12dfv 7021 f13dfv 7022 knatar 7099 ofrfval 7406 fmpox 7754 ovmptss 7777 marypha1lem 8885 supeq123d 8902 oieq1 8964 acneq 9457 isfin1a 9702 fpwwe2cbv 10040 fpwwe2lem2 10042 fpwwecbv 10054 fpwwelem 10055 eltskg 10160 elgrug 10202 cau3lem 14702 rlim 14840 ello1 14860 elo1 14871 caurcvg2 15022 caucvgb 15024 fsum2dlem 15113 fsumcom2 15117 fprod2dlem 15322 fprodcom2 15326 pcfac 16223 vdwpc 16304 rami 16339 prmgaplem7 16381 prdsval 16716 ismre 16849 isacs2 16912 acsfiel 16913 iscat 16931 iscatd 16932 catidex 16933 catideu 16934 cidfval 16935 cidval 16936 catlid 16942 catrid 16943 comfeq 16964 catpropd 16967 monfval 16990 issubc 17093 fullsubc 17108 isfunc 17122 funcpropd 17158 isfull 17168 isfth 17172 fthpropd 17179 natfval 17204 initoval 17245 termoval 17246 isposd 17553 lubfval 17576 glbfval 17589 ismgm 17841 issstrmgm 17851 grpidval 17859 gsumvalx 17874 gsumpropd 17876 gsumress 17880 issgrp 17890 ismnddef 17901 ismndd 17921 mndpropd 17924 ismhm 17946 resmhm 17973 isgrp 18047 grppropd 18056 isgrpd2e 18060 isnsg 18245 nmznsg 18258 isghm 18296 isga 18359 subgga 18368 gsmsymgrfix 18485 gsmsymgreq 18489 gexval 18632 ispgp 18646 isslw 18662 sylow2blem2 18675 efgval 18772 efgi 18774 efgsdm 18785 cmnpropd 18845 iscmnd 18848 submcmn2 18888 gsumzaddlem 18970 dmdprd 19049 dprdcntz 19059 issrg 19186 isring 19230 ringpropd 19261 isirred 19378 sdrgacs 19509 abvfval 19518 abvpropd 19542 islmod 19567 islmodd 19569 lmodprop2d 19625 lssset 19634 islmhm 19728 reslmhm 19753 lmhmpropd 19774 islbs 19777 rrgval 19988 isdomn 19995 isassa 20016 isassad 20024 assapropd 20029 ltbval 20180 opsrval 20183 psgndiflemA 20673 isphl 20700 islindf 20884 islindf2 20886 lsslindf 20902 dmatval 21029 dmatcrng 21039 scmatcrng 21058 cpmat 21245 istopg 21431 restbas 21694 ordtrest2 21740 cnfval 21769 cnpfval 21770 ist0 21856 ist1 21857 ishaus 21858 iscnrm 21859 isnrm 21871 ist0-2 21880 ishaus2 21887 nrmsep3 21891 iscmp 21924 is1stc 21977 isptfin 22052 islocfin 22053 kgenval 22071 kgencn2 22093 txbas 22103 ptval 22106 dfac14 22154 isfil 22383 isufil 22439 isufl 22449 flfcntr 22579 ucnval 22813 iscusp 22835 prdsxmslem2 23066 tngngp3 23192 isnlm 23211 nmofval 23250 lebnumii 23497 iscau4 23809 iscmet 23814 iscmet3lem1 23821 iscmet3 23823 equivcmet 23847 ulmcaulem 24909 ulmcau 24910 fsumdvdscom 25689 dchrisumlem3 25994 pntibndlem2 26094 pntibnd 26096 pntlemp 26113 ostth2lem2 26137 trgcgrg 26228 tgcgr4 26244 isismt 26247 nbgr2vtx1edg 27059 nbuhgr2vtx1edgb 27061 uvtxval 27096 uvtxel 27097 uvtxel1 27105 uvtxusgrel 27112 cusgredg 27133 cplgr3v 27144 cplgrop 27146 usgredgsscusgredg 27168 isrgr 27268 isewlk 27311 iswlk 27319 iswwlks 27541 wlkiswwlks2 27580 isclwwlk 27689 clwlkclwwlklem1 27704 isconngr 27895 isconngr1 27896 isfrgr 27966 frgr1v 27977 nfrgr2v 27978 frgr3v 27981 1vwmgr 27982 3vfriswmgr 27984 3cyclfrgrrn1 27991 n4cyclfrgr 27997 isplig 28180 gidval 28216 vciOLD 28265 isvclem 28281 isnvlem 28314 lnoval 28456 ajfval 28513 isphg 28521 minvecolem3 28580 htth 28622 ressprs 30569 isslmd 30757 resv1r 30837 prmidlval 30873 iscref 31007 ordtrest2NEW 31065 fmcncfil 31073 issiga 31270 isrnsiga 31271 isldsys 31314 ismeas 31357 carsgval 31460 issibf 31490 sitgfval 31498 signstfvneq0 31741 istrkg2d 31836 ispconn 32367 issconn 32370 txpconn 32376 cvxpconn 32386 cvmscbv 32402 iscvm 32403 cvmsdisj 32414 cvmsss2 32418 snmlval 32475 elmrsubrn 32664 ismfs 32693 mclsval 32707 frrlem4 33023 fwddifnval 33521 bj-ismoore 34291 pibp19 34577 pibp21 34578 poimirlem28 34801 cover2g 34871 seqpo 34903 incsequz2 34905 caushft 34917 ismtyval 34959 isass 35005 isexid 35006 elghomlem1OLD 35044 isrngo 35056 isrngod 35057 isgrpda 35114 rngohomval 35123 iscom2 35154 idlval 35172 pridlval 35192 maxidlval 35198 elrefrels3 35638 elcnvrefrels3 35651 eleqvrels3 35708 lflset 36075 islfld 36078 isopos 36196 isoml 36254 isatl 36315 iscvlat 36339 ishlat1 36368 psubspset 36760 lautset 37098 pautsetN 37114 ldilfset 37124 ltrnfset 37133 dilfsetN 37168 trnfsetN 37171 trnsetN 37172 trlfset 37176 tendofset 37774 tendoset 37775 dihffval 38246 lpolsetN 38498 hdmapfval 38843 hgmapfval 38902 aomclem8 39539 islnm 39555 clsk1independent 40274 gneispace2 40360 gneispaceel2 40372 gneispacess2 40374 ioodvbdlimc1lem1 42092 ioodvbdlimc1lem2 42093 ioodvbdlimc2lem 42095 issal 42476 ismea 42610 isome 42653 iccpartiltu 43459 iccelpart 43470 isomgr 43865 isupwlk 43888 mgmpropd 43919 ismgmd 43920 ismgmhm 43927 resmgmhm 43942 iscllaw 44024 iscomlaw 44025 isasslaw 44027 isrng 44075 c0snmgmhm 44113 zlidlring 44127 uzlidlring 44128 dmatALTval 44383 islininds 44429 lindslinindsimp2 44446 ldepsnlinc 44491 elbigo 44539 |
Copyright terms: Public domain | W3C validator |