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 2898 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
3 | raleqbidv.2 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 2, 3 | imbi12d 346 | . 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒))) |
5 | 4 | ralbidv2 3195 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ∈ wcel 2105 ∀wral 3138 |
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 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 df-clel 2893 df-ral 3143 |
This theorem is referenced by: raleqbi1dv 3404 rspc2vd 3931 f12dfv 7021 f13dfv 7022 knatar 7099 ofrfval 7406 fmpox 7756 ovmptss 7779 marypha1lem 8886 supeq123d 8903 oieq1 8965 acneq 9458 isfin1a 9703 fpwwe2cbv 10041 fpwwe2lem2 10043 fpwwecbv 10055 fpwwelem 10056 eltskg 10161 elgrug 10203 cau3lem 14704 rlim 14842 ello1 14862 elo1 14873 caurcvg2 15024 caucvgb 15026 fsum2dlem 15115 fsumcom2 15119 fprod2dlem 15324 fprodcom2 15328 pcfac 16225 vdwpc 16306 rami 16341 prmgaplem7 16383 prdsval 16718 ismre 16851 isacs2 16914 acsfiel 16915 iscat 16933 iscatd 16934 catidex 16935 catideu 16936 cidfval 16937 cidval 16938 catlid 16944 catrid 16945 comfeq 16966 catpropd 16969 monfval 16992 issubc 17095 fullsubc 17110 isfunc 17124 funcpropd 17160 isfull 17170 isfth 17174 fthpropd 17181 natfval 17206 initoval 17247 termoval 17248 isposd 17555 lubfval 17578 glbfval 17591 ismgm 17843 issstrmgm 17853 grpidval 17861 gsumvalx 17876 gsumpropd 17878 gsumress 17882 issgrp 17892 ismnddef 17903 ismndd 17923 mndpropd 17926 ismhm 17948 resmhm 17975 isgrp 18049 grppropd 18058 isgrpd2e 18062 isnsg 18247 nmznsg 18260 isghm 18298 isga 18361 subgga 18370 gsmsymgrfix 18487 gsmsymgreq 18491 gexval 18634 ispgp 18648 isslw 18664 sylow2blem2 18677 efgval 18774 efgi 18776 efgsdm 18787 cmnpropd 18847 iscmnd 18850 submcmn2 18890 gsumzaddlem 18972 dmdprd 19051 dprdcntz 19061 issrg 19188 isring 19232 ringpropd 19263 isirred 19380 sdrgacs 19511 abvfval 19520 abvpropd 19544 islmod 19569 islmodd 19571 lmodprop2d 19627 lssset 19636 islmhm 19730 reslmhm 19755 lmhmpropd 19776 islbs 19779 rrgval 19990 isdomn 19997 isassa 20018 isassad 20026 assapropd 20031 ltbval 20182 opsrval 20185 psgndiflemA 20675 isphl 20702 islindf 20886 islindf2 20888 lsslindf 20904 dmatval 21031 dmatcrng 21041 scmatcrng 21060 cpmat 21247 istopg 21433 restbas 21696 ordtrest2 21742 cnfval 21771 cnpfval 21772 ist0 21858 ist1 21859 ishaus 21860 iscnrm 21861 isnrm 21873 ist0-2 21882 ishaus2 21889 nrmsep3 21893 iscmp 21926 is1stc 21979 isptfin 22054 islocfin 22055 kgenval 22073 kgencn2 22095 txbas 22105 ptval 22108 dfac14 22156 isfil 22385 isufil 22441 isufl 22451 flfcntr 22581 ucnval 22815 iscusp 22837 prdsxmslem2 23068 tngngp3 23194 isnlm 23213 nmofval 23252 lebnumii 23499 iscau4 23811 iscmet 23816 iscmet3lem1 23823 iscmet3 23825 equivcmet 23849 ulmcaulem 24911 ulmcau 24912 fsumdvdscom 25690 dchrisumlem3 25995 pntibndlem2 26095 pntibnd 26097 pntlemp 26114 ostth2lem2 26138 trgcgrg 26229 tgcgr4 26245 isismt 26248 nbgr2vtx1edg 27060 nbuhgr2vtx1edgb 27062 uvtxval 27097 uvtxel 27098 uvtxel1 27106 uvtxusgrel 27113 cusgredg 27134 cplgr3v 27145 cplgrop 27147 usgredgsscusgredg 27169 isrgr 27269 isewlk 27312 iswlk 27320 iswwlks 27542 wlkiswwlks2 27581 isclwwlk 27690 clwlkclwwlklem1 27705 isconngr 27896 isconngr1 27897 isfrgr 27967 frgr1v 27978 nfrgr2v 27979 frgr3v 27982 1vwmgr 27983 3vfriswmgr 27985 3cyclfrgrrn1 27992 n4cyclfrgr 27998 isplig 28181 gidval 28217 vciOLD 28266 isvclem 28282 isnvlem 28315 lnoval 28457 ajfval 28514 isphg 28522 minvecolem3 28581 htth 28623 ressprs 30570 isslmd 30758 resv1r 30838 prmidlval 30874 iscref 31008 ordtrest2NEW 31066 fmcncfil 31074 issiga 31271 isrnsiga 31272 isldsys 31315 ismeas 31358 carsgval 31461 issibf 31491 sitgfval 31499 signstfvneq0 31742 istrkg2d 31837 ispconn 32368 issconn 32371 txpconn 32377 cvxpconn 32387 cvmscbv 32403 iscvm 32404 cvmsdisj 32415 cvmsss2 32419 snmlval 32476 elmrsubrn 32665 ismfs 32694 mclsval 32708 frrlem4 33024 fwddifnval 33522 bj-ismoore 34292 pibp19 34578 pibp21 34579 poimirlem28 34802 cover2g 34873 seqpo 34905 incsequz2 34907 caushft 34919 ismtyval 34961 isass 35007 isexid 35008 elghomlem1OLD 35046 isrngo 35058 isrngod 35059 isgrpda 35116 rngohomval 35125 iscom2 35156 idlval 35174 pridlval 35194 maxidlval 35200 elrefrels3 35640 elcnvrefrels3 35653 eleqvrels3 35710 lflset 36077 islfld 36080 isopos 36198 isoml 36256 isatl 36317 iscvlat 36341 ishlat1 36370 psubspset 36762 lautset 37100 pautsetN 37116 ldilfset 37126 ltrnfset 37135 dilfsetN 37170 trnfsetN 37173 trnsetN 37174 trlfset 37178 tendofset 37776 tendoset 37777 dihffval 38248 lpolsetN 38500 hdmapfval 38845 hgmapfval 38904 aomclem8 39541 islnm 39557 clsk1independent 40276 gneispace2 40362 gneispaceel2 40374 gneispacess2 40376 ioodvbdlimc1lem1 42096 ioodvbdlimc1lem2 42097 ioodvbdlimc2lem 42099 issal 42480 ismea 42614 isome 42657 iccpartiltu 43429 iccelpart 43440 isomgr 43835 isupwlk 43858 mgmpropd 43889 ismgmd 43890 ismgmhm 43897 resmgmhm 43912 iscllaw 43994 iscomlaw 43995 isasslaw 43997 isrng 44045 c0snmgmhm 44083 zlidlring 44097 uzlidlring 44098 dmatALTval 44353 islininds 44399 lindslinindsimp2 44416 ldepsnlinc 44461 elbigo 44509 |
Copyright terms: Public domain | W3C validator |