![]() |
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 2129, ax-11 2146, and ax-12 2166 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 2811 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
3 | raleqbidv.2 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 2, 3 | imbi12d 343 | . 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒))) |
5 | 4 | ralbidv2 3163 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1533 ∈ wcel 2098 ∀wral 3050 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-cleq 2717 df-clel 2802 df-ral 3051 |
This theorem is referenced by: rspc2vd 3940 frd 5637 f12dfv 7282 f13dfv 7283 knatar 7364 ofrfvalg 7693 fmpox 8072 ovmptss 8098 frrlem4 8295 on2ind 8690 on3ind 8691 marypha1lem 9458 supeq123d 9475 oieq1 9537 acneq 10068 isfin1a 10317 fpwwe2cbv 10655 fpwwe2lem2 10657 fpwwecbv 10669 fpwwelem 10670 eltskg 10775 elgrug 10817 cau3lem 15337 rlim 15475 ello1 15495 elo1 15506 caurcvg2 15660 caucvgb 15662 fsum2dlem 15752 fsumcom2 15756 fprod2dlem 15960 fprodcom2 15964 pcfac 16871 vdwpc 16952 rami 16987 prmgaplem7 17029 prdsval 17440 ismre 17573 isacs2 17636 acsfiel 17637 iscat 17655 iscatd 17656 catidex 17657 catideu 17658 cidfval 17659 cidval 17660 catlid 17666 catrid 17667 comfeq 17689 catpropd 17692 monfval 17718 issubc 17824 fullsubc 17839 isfunc 17853 funcpropd 17892 isfull 17902 isfth 17906 fthpropd 17913 natfval 17939 initoval 17985 termoval 17986 isposd 18318 lubfval 18345 glbfval 18358 ismgm 18604 mgmpropd 18614 ismgmd 18615 issstrmgm 18616 grpidval 18624 gsumvalx 18639 gsumpropd 18641 gsumress 18645 ismgmhm 18659 resmgmhm 18674 issgrp 18683 sgrppropd 18694 ismnddef 18699 ismndd 18719 mndpropd 18722 ismhm 18745 resmhm 18780 isgrp 18904 grppropd 18916 isgrpd2e 18920 isnsg 19118 nmznsg 19131 isghm 19178 isghmOLD 19179 isga 19254 subgga 19263 gsmsymgrfix 19395 gsmsymgreq 19399 gexval 19545 ispgp 19559 isslw 19575 sylow2blem2 19588 efgval 19684 efgi 19686 efgsdm 19697 cmnpropd 19758 iscmnd 19761 submcmn2 19806 gsumzaddlem 19888 dmdprd 19967 dprdcntz 19977 isrng 20106 rngpropd 20126 issrg 20140 isring 20189 ringpropd 20236 isirred 20370 c0snmgmhm 20413 islring 20489 sdrgacs 20701 abvfval 20710 abvpropd 20734 islmod 20759 islmodd 20761 lmodprop2d 20819 lssset 20829 islmhm 20924 reslmhm 20949 lmhmpropd 20970 islbs 20973 rrgval 21251 isdomn 21258 psgndiflemA 21550 isphl 21577 islindf 21763 islindf2 21765 lsslindf 21781 isassa 21807 isassad 21815 assapropd 21822 ltbval 22003 opsrval 22006 dmatval 22438 dmatcrng 22448 scmatcrng 22467 cpmat 22655 istopg 22841 restbas 23106 ordtrest2 23152 cnfval 23181 cnpfval 23182 ist0 23268 ist1 23269 ishaus 23270 iscnrm 23271 isnrm 23283 ist0-2 23292 ishaus2 23299 nrmsep3 23303 iscmp 23336 is1stc 23389 isptfin 23464 islocfin 23465 kgenval 23483 kgencn2 23505 txbas 23515 ptval 23518 dfac14 23566 isfil 23795 isufil 23851 isufl 23861 flfcntr 23991 ucnval 24226 iscusp 24248 prdsxmslem2 24482 tngngp3 24617 isnlm 24636 nmofval 24675 lebnumii 24936 iscau4 25251 iscmet 25256 iscmet3lem1 25263 iscmet3 25265 equivcmet 25289 ulmcaulem 26375 ulmcau 26376 fsumdvdscom 27162 dchrisumlem3 27469 pntibndlem2 27569 pntibnd 27571 pntlemp 27588 ostth2lem2 27612 madebdayim 27860 no2indslem 27917 no3inds 27921 istrkgc 28330 istrkgb 28331 istrkge 28333 trgcgrg 28391 tgcgr4 28407 isismt 28410 nbgr2vtx1edg 29235 nbuhgr2vtx1edgb 29237 uvtxval 29272 uvtxel 29273 uvtxel1 29281 uvtxusgrel 29288 cusgredg 29309 cplgr3v 29320 cplgrop 29322 usgredgsscusgredg 29345 isrgr 29445 isewlk 29488 iswlk 29496 iswwlks 29719 wlkiswwlks2 29758 isclwwlk 29866 clwlkclwwlklem1 29881 isconngr 30071 isconngr1 30072 isfrgr 30142 frgr1v 30153 nfrgr2v 30154 frgr3v 30157 1vwmgr 30158 3vfriswmgr 30160 3cyclfrgrrn1 30167 n4cyclfrgr 30173 isplig 30358 gidval 30394 vciOLD 30443 isvclem 30459 isnvlem 30492 lnoval 30634 ajfval 30691 isphg 30699 minvecolem3 30758 htth 30800 ressprs 32779 mntoval 32798 mgcoval 32802 isslmd 33001 resv1r 33152 prmidlval 33249 mxidlval 33273 rprmval 33328 isufd 33352 iscref 33573 ordtrest2NEW 33652 fmcncfil 33660 issiga 33859 isrnsiga 33860 isldsys 33903 ismeas 33946 carsgval 34051 issibf 34081 sitgfval 34089 signstfvneq0 34332 istrkg2d 34426 ispconn 34961 issconn 34964 txpconn 34970 cvxpconn 34980 cvmscbv 34996 iscvm 34997 cvmsdisj 35008 cvmsss2 35012 snmlval 35069 elmrsubrn 35258 ismfs 35287 mclsval 35301 fwddifnval 35887 bj-ismoore 36712 pibp19 37021 pibp21 37022 poimirlem28 37249 cover2g 37317 seqpo 37348 incsequz2 37350 caushft 37362 ismtyval 37401 isass 37447 isexid 37448 elghomlem1OLD 37486 isrngo 37498 isrngod 37499 isgrpda 37556 rngohomval 37565 iscom2 37596 idlval 37614 pridlval 37634 maxidlval 37640 elrefrels3 38118 elcnvrefrels3 38134 eleqvrels3 38192 lflset 38658 islfld 38661 isopos 38779 isoml 38837 isatl 38898 iscvlat 38922 ishlat1 38951 psubspset 39344 lautset 39682 pautsetN 39698 ldilfset 39708 ltrnfset 39717 dilfsetN 39752 trnfsetN 39755 trnsetN 39756 trlfset 39760 tendofset 40358 tendoset 40359 dihffval 40830 lpolsetN 41082 hdmapfval 41427 hgmapfval 41486 sn-isghm 42229 aomclem8 42624 islnm 42640 clsk1independent 43615 gneispace2 43701 gneispaceel2 43713 gneispacess2 43715 caucvgbf 45007 ioodvbdlimc1lem1 45454 ioodvbdlimc1lem2 45455 ioodvbdlimc2lem 45457 issal 45837 ismea 45974 isome 46017 iccpartiltu 46896 iccelpart 46907 isgrim 47349 isupwlk 47381 iscllaw 47434 iscomlaw 47435 isasslaw 47437 zlidlring 47479 uzlidlring 47480 dmatALTval 47651 islininds 47697 lindslinindsimp2 47714 ldepsnlinc 47759 elbigo 47807 iscnrm3r 48150 isprsd 48157 lubeldm2d 48160 glbeldm2d 48161 isthincd2lem2 48225 isthincd 48226 |
Copyright terms: Public domain | W3C validator |