![]() |
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 3168 | . 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | ralbidv 3168 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wral 3051 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ral 3052 |
This theorem is referenced by: 3ralbidv 3212 6ralbidv 3214 cbvral3vw 3231 cbvral6vw 3233 cbvral3v 3354 rspc6v 3628 ralxpxfr2d 3631 poeq1 5597 soeq1 5615 isoeq1 7329 isoeq2 7330 isoeq3 7331 fnmpoovd 8101 xpord3inddlem 8168 smoeq 8380 xpf1o 9177 nqereu 10972 dedekind 11427 dedekindle 11428 seqcaopr2 14058 wrd2ind 14731 addcn2 15596 mulcn2 15598 mreexexd 17661 catlid 17696 catrid 17697 isfunc 17883 funcres2b 17916 isfull 17932 isfth 17936 fullres2c 17961 isnat 17970 evlfcl 18247 uncfcurf 18264 isprs 18322 isdrs 18326 ispos 18339 istos 18443 isdlat 18547 ismgmhm 18689 issubmgm 18695 sgrp1 18722 ismhm 18775 issubm 18793 sgrp2nmndlem4 18918 isnsg 19149 isghm 19209 isghmOLD 19210 isga 19285 pmtrdifwrdel 19483 sylow2blem2 19619 efglem 19714 efgi 19717 efgredlemb 19744 efgred 19746 frgpuplem 19770 iscmn 19787 ring1 20289 isirred 20401 rnghmval 20422 isrnghm 20423 islmod 20840 lmodlema 20841 lssset 20910 islssd 20912 islmhm 21005 islmhm2 21016 isobs 21718 dmatel 22486 dmatmulcl 22493 scmateALT 22505 mdetunilem3 22607 mdetunilem4 22608 mdetunilem9 22613 cpmatel 22704 chpscmat 22835 hausnei2 23348 dfconn2 23414 llyeq 23465 nllyeq 23466 isucn2 24275 iducn 24279 ispsmet 24301 ismet 24320 isxmet 24321 metucn 24571 ngptgp 24636 nlmvscnlem1 24694 xmetdcn2 24844 addcnlem 24871 elcncf 24900 ipcnlem1 25264 cfili 25287 c1lip1 26021 aalioulem5 26364 aalioulem6 26365 aaliou 26366 aaliou2 26368 aaliou2b 26369 ulmcau 26424 ulmdvlem3 26431 cxpcn3lem 26775 mpodvdsmulf1o 27222 dvdsmulf1o 27224 chpdifbndlem2 27583 pntrsumbnd2 27596 addsprop 27990 negsprop 28044 istrkgb 28382 axtgsegcon 28391 axtg5seg 28392 axtgpasch 28394 axtgeucl 28399 iscgrg 28439 isismt 28461 isperp2 28642 f1otrg 28798 axcontlem10 28907 axcontlem12 28909 iscusgredg 29359 isgrpo 30430 isablo 30479 vacn 30627 smcnlem 30630 lnoval 30685 islno 30686 isphg 30750 ajmoi 30791 ajval 30794 adjmo 31765 elcnop 31790 ellnop 31791 elunop 31805 elhmop 31806 elcnfn 31815 ellnfn 31816 adjeu 31822 adjval 31823 adj1 31866 adjeq 31868 cnlnadjlem9 32008 cnlnadjeu 32011 cnlnssadj 32013 isst 32146 ishst 32147 cdj1i 32366 cdj3i 32374 resspos 32836 resstos 32837 ismnt 32853 mgcval 32857 isomnd 32936 isslmd 33066 slmdlema 33067 isorng 33177 prmidlval 33312 isprmidl 33313 isrprm 33392 qqhucn 33807 ismntop 33841 axtgupdim2ALTV 34514 txpconn 35060 nn0prpw 36035 heicant 37356 equivbnd 37491 isismty 37502 heibor1lem 37510 iccbnd 37541 isass 37547 elghomlem1OLD 37586 elghomlem2OLD 37587 isrngohom 37666 iscom2 37696 pridlval 37734 ispridl 37735 isdmn3 37775 inecmo 38053 islfl 38758 isopos 38878 psubspset 39443 islaut 39782 ispautN 39798 ltrnset 39817 isltrn 39818 istrnN 39856 istendo 40459 sticksstones1 41844 sticksstones2 41845 sticksstones3 41846 sticksstones8 41851 sticksstones10 41853 sticksstones11 41854 sticksstones12a 41855 sticksstones15 41859 sn-isghm 42327 clsk1independent 43713 sprsymrelfolem2 47065 sprsymrelfo 47069 reuopreuprim 47098 dmatALTbasel 47785 lindslinindsimp2 47846 lmod1 47875 isnrm4 48264 iscnrm4 48288 isthinc 48342 thincciso 48370 |
Copyright terms: Public domain | W3C validator |