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 3115 | . 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | ralbidv 3115 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∀wral 3058 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ral 3063 |
This theorem is referenced by: cbvral3vw 3370 cbvral3v 3373 ralxpxfr2d 3550 poeq1 5468 soeq1 5486 isoeq1 7123 isoeq2 7124 isoeq3 7125 fnmpoovd 7852 smoeq 8084 xpf1o 8805 nqereu 10540 dedekind 10992 dedekindle 10993 seqcaopr2 13609 wrd2ind 14285 addcn2 15152 mulcn2 15154 mreexexd 17148 catlid 17183 catrid 17184 isfunc 17367 funcres2b 17400 isfull 17414 isfth 17418 fullres2c 17443 isnat 17451 evlfcl 17727 uncfcurf 17744 isprs 17801 isdrs 17805 ispos 17818 istos 17921 isdlat 18025 sgrp1 18169 ismhm 18217 issubm 18227 sgrp2nmndlem4 18352 isnsg 18568 isghm 18619 isga 18682 pmtrdifwrdel 18874 sylow2blem2 19007 efglem 19103 efgi 19106 efgredlemb 19133 efgred 19135 frgpuplem 19159 iscmn 19175 ring1 19617 isirred 19714 islmod 19900 lmodlema 19901 lssset 19967 islssd 19969 islmhm 20061 islmhm2 20072 isobs 20679 dmatel 21387 dmatmulcl 21394 scmateALT 21406 mdetunilem3 21508 mdetunilem4 21509 mdetunilem9 21514 cpmatel 21605 chpscmat 21736 hausnei2 22247 dfconn2 22313 llyeq 22364 nllyeq 22365 isucn2 23173 iducn 23177 ispsmet 23199 ismet 23218 isxmet 23219 metucn 23466 ngptgp 23531 nlmvscnlem1 23581 xmetdcn2 23731 addcnlem 23758 elcncf 23783 ipcnlem1 24139 cfili 24162 c1lip1 24891 aalioulem5 25226 aalioulem6 25227 aaliou 25228 aaliou2 25230 aaliou2b 25231 ulmcau 25284 ulmdvlem3 25291 cxpcn3lem 25630 dvdsmulf1o 26073 chpdifbndlem2 26432 pntrsumbnd2 26445 istrkgb 26543 axtgsegcon 26552 axtg5seg 26553 axtgpasch 26555 axtgeucl 26560 iscgrg 26600 isismt 26622 isperp2 26803 f1otrg 26959 axcontlem10 27061 axcontlem12 27063 iscusgredg 27508 isgrpo 28575 isablo 28624 vacn 28772 smcnlem 28775 lnoval 28830 islno 28831 isphg 28895 ajmoi 28936 ajval 28939 adjmo 29910 elcnop 29935 ellnop 29936 elunop 29950 elhmop 29951 elcnfn 29960 ellnfn 29961 adjeu 29967 adjval 29968 adj1 30011 adjeq 30013 cnlnadjlem9 30153 cnlnadjeu 30156 cnlnssadj 30158 isst 30291 ishst 30292 cdj1i 30511 cdj3i 30519 resspos 30960 resstos 30961 ismnt 30977 mgcval 30981 isomnd 31043 isslmd 31171 slmdlema 31172 isorng 31214 prmidlval 31323 isprmidl 31324 isrprm 31376 qqhucn 31651 ismntop 31685 axtgupdim2ALTV 32357 txpconn 32904 xpord3ind 33534 nn0prpw 34246 heicant 35547 equivbnd 35683 isismty 35694 heibor1lem 35702 iccbnd 35733 isass 35739 elghomlem1OLD 35778 elghomlem2OLD 35779 isrngohom 35858 iscom2 35888 pridlval 35926 ispridl 35927 isdmn3 35967 inecmo 36222 islfl 36809 isopos 36929 psubspset 37493 islaut 37832 ispautN 37848 ltrnset 37867 isltrn 37868 istrnN 37906 istendo 38509 sticksstones1 39822 sticksstones2 39823 sticksstones3 39824 sticksstones8 39829 sticksstones10 39831 sticksstones11 39832 sticksstones12a 39833 sticksstones15 39837 clsk1independent 41331 sprsymrelfolem2 44616 sprsymrelfo 44620 reuopreuprim 44649 ismgmhm 45008 issubmgm 45014 rnghmval 45120 isrnghm 45121 lidlmsgrp 45155 lidlrng 45156 dmatALTbasel 45414 lindslinindsimp2 45475 lmod1 45504 isnrm4 45895 iscnrm4 45919 isthinc 45973 thincciso 46001 |
Copyright terms: Public domain | W3C validator |