![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2ralbidv | Structured version Visualization version GIF version |
Description: Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.) |
Ref | Expression |
---|---|
2ralbidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
2ralbidv | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2ralbidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | ralbidv 3171 | . 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | ralbidv 3171 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wral 3061 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ral 3062 |
This theorem is referenced by: 3ralbidv 3212 cbvral3vw 3228 cbvral3v 3342 ralxpxfr2d 3597 poeq1 5549 soeq1 5567 isoeq1 7263 isoeq2 7264 isoeq3 7265 fnmpoovd 8020 xpord3inddlem 8087 smoeq 8297 xpf1o 9086 nqereu 10870 dedekind 11323 dedekindle 11324 seqcaopr2 13950 wrd2ind 14617 addcn2 15482 mulcn2 15484 mreexexd 17533 catlid 17568 catrid 17569 isfunc 17755 funcres2b 17788 isfull 17802 isfth 17806 fullres2c 17831 isnat 17839 evlfcl 18116 uncfcurf 18133 isprs 18191 isdrs 18195 ispos 18208 istos 18312 isdlat 18416 sgrp1 18560 ismhm 18608 issubm 18619 sgrp2nmndlem4 18743 isnsg 18962 isghm 19013 isga 19076 pmtrdifwrdel 19272 sylow2blem2 19408 efglem 19503 efgi 19506 efgredlemb 19533 efgred 19535 frgpuplem 19559 iscmn 19576 ring1 20031 isirred 20135 islmod 20340 lmodlema 20341 lssset 20409 islssd 20411 islmhm 20503 islmhm2 20514 isobs 21142 dmatel 21858 dmatmulcl 21865 scmateALT 21877 mdetunilem3 21979 mdetunilem4 21980 mdetunilem9 21985 cpmatel 22076 chpscmat 22207 hausnei2 22720 dfconn2 22786 llyeq 22837 nllyeq 22838 isucn2 23647 iducn 23651 ispsmet 23673 ismet 23692 isxmet 23693 metucn 23943 ngptgp 24008 nlmvscnlem1 24066 xmetdcn2 24216 addcnlem 24243 elcncf 24268 ipcnlem1 24625 cfili 24648 c1lip1 25377 aalioulem5 25712 aalioulem6 25713 aaliou 25714 aaliou2 25716 aaliou2b 25717 ulmcau 25770 ulmdvlem3 25777 cxpcn3lem 26116 dvdsmulf1o 26559 chpdifbndlem2 26918 pntrsumbnd2 26931 addsprop 27310 negsprop 27355 istrkgb 27439 axtgsegcon 27448 axtg5seg 27449 axtgpasch 27451 axtgeucl 27456 iscgrg 27496 isismt 27518 isperp2 27699 f1otrg 27855 axcontlem10 27964 axcontlem12 27966 iscusgredg 28413 isgrpo 29481 isablo 29530 vacn 29678 smcnlem 29681 lnoval 29736 islno 29737 isphg 29801 ajmoi 29842 ajval 29845 adjmo 30816 elcnop 30841 ellnop 30842 elunop 30856 elhmop 30857 elcnfn 30866 ellnfn 30867 adjeu 30873 adjval 30874 adj1 30917 adjeq 30919 cnlnadjlem9 31059 cnlnadjeu 31062 cnlnssadj 31064 isst 31197 ishst 31198 cdj1i 31417 cdj3i 31425 resspos 31875 resstos 31876 ismnt 31892 mgcval 31896 isomnd 31958 isslmd 32086 slmdlema 32087 isorng 32141 prmidlval 32257 isprmidl 32258 isrprm 32310 qqhucn 32630 ismntop 32664 axtgupdim2ALTV 33338 txpconn 33883 nn0prpw 34841 heicant 36159 equivbnd 36295 isismty 36306 heibor1lem 36314 iccbnd 36345 isass 36351 elghomlem1OLD 36390 elghomlem2OLD 36391 isrngohom 36470 iscom2 36500 pridlval 36538 ispridl 36539 isdmn3 36579 inecmo 36862 islfl 37568 isopos 37688 psubspset 38253 islaut 38592 ispautN 38608 ltrnset 38627 isltrn 38628 istrnN 38666 istendo 39269 sticksstones1 40600 sticksstones2 40601 sticksstones3 40602 sticksstones8 40607 sticksstones10 40609 sticksstones11 40610 sticksstones12a 40611 sticksstones15 40615 clsk1independent 42406 sprsymrelfolem2 45771 sprsymrelfo 45775 reuopreuprim 45804 ismgmhm 46163 issubmgm 46169 rnghmval 46275 isrnghm 46276 lidlmsgrp 46310 lidlrng 46311 dmatALTbasel 46569 lindslinindsimp2 46630 lmod1 46659 isnrm4 47049 iscnrm4 47073 isthinc 47127 thincciso 47155 |
Copyright terms: Public domain | W3C validator |