Theorem 2ralbidv 3218

Description: Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.)

Hypothesis

Ref	Expression
2ralbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
2ralbidv	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem 2ralbidv

Step	Hyp	Ref	Expression
1		2ralbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	ralbidv 3177	. 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
3	2	ralbidv 3177	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

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 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3062

This theorem is referenced by:  3ralbidv  3221  6ralbidv  3223  cbvral3vw  3240  cbvral6vw  3242  cbvral3v  3366  rspc6v  3631  ralxpxfr2d  3634  poeq1  5591  soeq1  5609  isoeq1  7313  isoeq2  7314  isoeq3  7315  fnmpoovd  8072  xpord3inddlem  8139  smoeq  8349  xpf1o  9138  nqereu  10923  dedekind  11376  dedekindle  11377  seqcaopr2  14003  wrd2ind  14672  addcn2  15537  mulcn2  15539  mreexexd  17591  catlid  17626  catrid  17627  isfunc  17813  funcres2b  17846  isfull  17860  isfth  17864  fullres2c  17889  isnat  17897  evlfcl  18174  uncfcurf  18191  isprs  18249  isdrs  18253  ispos  18266  istos  18370  isdlat  18474  sgrp1  18619  ismhm  18672  issubm  18683  sgrp2nmndlem4  18808  isnsg  19034  isghm  19091  isga  19154  pmtrdifwrdel  19352  sylow2blem2  19488  efglem  19583  efgi  19586  efgredlemb  19613  efgred  19615  frgpuplem  19639  iscmn  19656  ring1  20121  isirred  20232  islmod  20474  lmodlema  20475  lssset  20543  islssd  20545  islmhm  20637  islmhm2  20648  isobs  21274  dmatel  21994  dmatmulcl  22001  scmateALT  22013  mdetunilem3  22115  mdetunilem4  22116  mdetunilem9  22121  cpmatel  22212  chpscmat  22343  hausnei2  22856  dfconn2  22922  llyeq  22973  nllyeq  22974  isucn2  23783  iducn  23787  ispsmet  23809  ismet  23828  isxmet  23829  metucn  24079  ngptgp  24144  nlmvscnlem1  24202  xmetdcn2  24352  addcnlem  24379  elcncf  24404  ipcnlem1  24761  cfili  24784  c1lip1  25513  aalioulem5  25848  aalioulem6  25849  aaliou  25850  aaliou2  25852  aaliou2b  25853  ulmcau  25906  ulmdvlem3  25913  cxpcn3lem  26252  dvdsmulf1o  26695  chpdifbndlem2  27054  pntrsumbnd2  27067  addsprop  27457  negsprop  27506  istrkgb  27703  axtgsegcon  27712  axtg5seg  27713  axtgpasch  27715  axtgeucl  27720  iscgrg  27760  isismt  27782  isperp2  27963  f1otrg  28119  axcontlem10  28228  axcontlem12  28230  iscusgredg  28677  isgrpo  29745  isablo  29794  vacn  29942  smcnlem  29945  lnoval  30000  islno  30001  isphg  30065  ajmoi  30106  ajval  30109  adjmo  31080  elcnop  31105  ellnop  31106  elunop  31120  elhmop  31121  elcnfn  31130  ellnfn  31131  adjeu  31137  adjval  31138  adj1  31181  adjeq  31183  cnlnadjlem9  31323  cnlnadjeu  31326  cnlnssadj  31328  isst  31461  ishst  31462  cdj1i  31681  cdj3i  31689  resspos  32131  resstos  32132  ismnt  32148  mgcval  32152  isomnd  32214  isslmd  32342  slmdlema  32343  isorng  32412  prmidlval  32550  isprmidl  32551  isrprm  32629  qqhucn  32967  ismntop  33001  axtgupdim2ALTV  33675  txpconn  34218  nn0prpw  35203  heicant  36518  equivbnd  36653  isismty  36664  heibor1lem  36672  iccbnd  36703  isass  36709  elghomlem1OLD  36748  elghomlem2OLD  36749  isrngohom  36828  iscom2  36858  pridlval  36896  ispridl  36897  isdmn3  36937  inecmo  37219  islfl  37925  isopos  38045  psubspset  38610  islaut  38949  ispautN  38965  ltrnset  38984  isltrn  38985  istrnN  39023  istendo  39626  sticksstones1  40957  sticksstones2  40958  sticksstones3  40959  sticksstones8  40964  sticksstones10  40966  sticksstones11  40967  sticksstones12a  40968  sticksstones15  40972  clsk1independent  42787  sprsymrelfolem2  46151  sprsymrelfo  46155  reuopreuprim  46184  ismgmhm  46543  issubmgm  46549  rnghmval  46679  isrnghm  46680  dmatALTbasel  47073  lindslinindsimp2  47134  lmod1  47163  isnrm4  47553  iscnrm4  47577  isthinc  47631  thincciso  47659