![]() |
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 3166 | . 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | ralbidv 3166 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∀wral 3107 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ral 3112 |
This theorem is referenced by: cbvral3v 3416 ralxpxfr2d 3580 poeq1 5372 soeq1 5389 isoeq1 6940 isoeq2 6941 isoeq3 6942 fnmpoovd 7645 smoeq 7846 xpf1o 8533 nqereu 10204 dedekind 10656 dedekindle 10657 seqcaopr2 13260 wrd2ind 13925 addcn2 14788 mulcn2 14790 mreexexd 16752 catlid 16787 catrid 16788 isfunc 16967 funcres2b 17000 isfull 17013 isfth 17017 fullres2c 17042 isnat 17050 evlfcl 17305 uncfcurf 17322 isprs 17373 isdrs 17377 ispos 17390 istos 17478 isdlat 17636 sgrp1 17736 ismhm 17780 issubm 17790 sgrp2nmndlem4 17858 isnsg 18066 isghm 18103 isga 18166 pmtrdifwrdel 18348 sylow2blem2 18480 efglem 18573 efgi 18576 efgredlemb 18603 efgred 18605 frgpuplem 18629 iscmn 18644 ring1 19046 isirred 19143 islmod 19332 lmodlema 19333 lssset 19399 islssd 19401 islmhm 19493 islmhm2 19504 isobs 20550 dmatel 20790 dmatmulcl 20797 scmateALT 20809 mdetunilem3 20911 mdetunilem4 20912 mdetunilem9 20917 cpmatel 21007 chpscmat 21138 hausnei2 21649 dfconn2 21715 llyeq 21766 nllyeq 21767 isucn2 22575 iducn 22579 ispsmet 22601 ismet 22620 isxmet 22621 metucn 22868 ngptgp 22932 nlmvscnlem1 22982 xmetdcn2 23132 addcnlem 23159 elcncf 23184 ipcnlem1 23535 cfili 23558 c1lip1 24281 aalioulem5 24612 aalioulem6 24613 aaliou 24614 aaliou2 24616 aaliou2b 24617 ulmcau 24670 ulmdvlem3 24677 cxpcn3lem 25013 dvdsmulf1o 25457 chpdifbndlem2 25816 pntrsumbnd2 25829 istrkgb 25927 axtgsegcon 25936 axtg5seg 25937 axtgpasch 25939 axtgeucl 25944 iscgrg 25984 isismt 26006 isperp2 26187 f1otrg 26344 axcontlem10 26446 axcontlem12 26448 iscusgredg 26892 isgrpo 27961 isablo 28010 vacn 28158 smcnlem 28161 lnoval 28216 islno 28217 isphg 28281 ajmoi 28322 ajval 28325 adjmo 29296 elcnop 29321 ellnop 29322 elunop 29336 elhmop 29337 elcnfn 29346 ellnfn 29347 adjeu 29353 adjval 29354 adj1 29397 adjeq 29399 cnlnadjlem9 29539 cnlnadjeu 29542 cnlnssadj 29544 isst 29677 ishst 29678 cdj1i 29897 cdj3i 29905 resspos 30316 resstos 30317 isomnd 30358 isslmd 30464 slmdlema 30465 isorng 30522 qqhucn 30846 ismntop 30880 axtgupdim2ALTV 31552 txpconn 32089 nn0prpw 33282 heicant 34479 equivbnd 34621 isismty 34632 heibor1lem 34640 iccbnd 34671 isass 34677 elghomlem1OLD 34716 elghomlem2OLD 34717 isrngohom 34796 iscom2 34826 pridlval 34864 ispridl 34865 isdmn3 34905 inecmo 35162 islfl 35748 isopos 35868 psubspset 36432 islaut 36771 ispautN 36787 ltrnset 36806 isltrn 36807 istrnN 36845 istendo 37448 clsk1independent 39902 sprsymrelfolem2 43159 sprsymrelfo 43163 reuopreuprim 43192 ismgmhm 43554 issubmgm 43560 rnghmval 43662 isrnghm 43663 lidlmsgrp 43697 lidlrng 43698 dmatALTbasel 43959 lindslinindsimp2 44020 lmod1 44049 |
Copyright terms: Public domain | W3C validator |