Theorem 2ralbidv 3202

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 3161	. 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒))
3	2	ralbidv 3161	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3052

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 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3053

This theorem is referenced by:  3ralbidv  3205  6ralbidv  3207  cbvral3vw  3222  cbvral6vw  3224  cbvral3v  3342  rspc6v  3599  ralxpxfr2d  3602  poeq1  5545  soeq1  5563  isoeq1  7275  isoeq2  7276  isoeq3  7277  fnmpoovd  8041  xpord3inddlem  8108  smoeq  8294  xpf1o  9081  nqereu  10854  dedekind  11310  dedekindle  11311  seqcaopr2  13975  wrd2ind  14660  addcn2  15531  mulcn2  15533  mreexexd  17585  catlid  17620  catrid  17621  isfunc  17802  funcres2b  17835  isfull  17850  isfth  17854  fullres2c  17879  isnat  17888  evlfcl  18159  uncfcurf  18176  isprs  18233  isdrs  18238  ispos  18251  istos  18353  resspos  18366  resstos  18367  isdlat  18459  ismgmhm  18635  issubmgm  18641  sgrp1  18668  ismhm  18724  issubm  18742  sgrp2nmndlem4  18870  isnsg  19101  isghm  19161  isghmOLD  19162  isga  19237  pmtrdifwrdel  19431  sylow2blem2  19567  efglem  19662  efgi  19665  efgredlemb  19692  efgred  19694  frgpuplem  19718  iscmn  19735  isomnd  20069  ring1  20262  isirred  20372  rnghmval  20393  isrnghm  20394  isorng  20811  islmod  20832  lmodlema  20833  lssset  20901  islssd  20903  islmhm  20996  islmhm2  21007  isobs  21692  dmatel  22454  dmatmulcl  22461  scmateALT  22473  mdetunilem3  22575  mdetunilem4  22576  mdetunilem9  22581  cpmatel  22672  chpscmat  22803  hausnei2  23314  dfconn2  23380  llyeq  23431  nllyeq  23432  isucn2  24239  iducn  24243  ispsmet  24265  ismet  24284  isxmet  24285  metucn  24532  ngptgp  24597  nlmvscnlem1  24647  xmetdcn2  24799  addcnlem  24826  elcncf  24855  ipcnlem1  25218  cfili  25241  c1lip1  25975  aalioulem5  26317  aalioulem6  26318  aaliou  26319  aaliou2  26321  aaliou2b  26322  ulmcau  26377  ulmdvlem3  26384  cxpcn3lem  26730  mpodvdsmulf1o  27177  dvdsmulf1o  27179  chpdifbndlem2  27538  pntrsumbnd2  27551  addsprop  27989  negsprop  28048  istrkgb  28544  axtgsegcon  28554  axtg5seg  28555  axtgpasch  28557  axtgeucl  28562  iscgrg  28602  isismt  28624  isperp2  28805  f1otrg  28961  axcontlem10  29064  axcontlem12  29066  iscusgredg  29514  isgrpo  30591  isablo  30640  vacn  30788  smcnlem  30791  lnoval  30846  islno  30847  isphg  30911  ajmoi  30952  ajval  30955  adjmo  31926  elcnop  31951  ellnop  31952  elunop  31966  elhmop  31967  elcnfn  31976  ellnfn  31977  adjeu  31983  adjval  31984  adj1  32027  adjeq  32029  cnlnadjlem9  32169  cnlnadjeu  32172  cnlnssadj  32174  isst  32307  ishst  32308  cdj1i  32527  cdj3i  32535  ismnt  33082  mgcval  33086  isslmd  33302  slmdlema  33303  prmidlval  33536  isprmidl  33537  isrprm  33616  qqhucn  34176  ismntop  34210  axtgupdim2ALTV  34852  txpconn  35454  nn0prpw  36545  heicant  37935  equivbnd  38070  isismty  38081  heibor1lem  38089  iccbnd  38120  isass  38126  elghomlem1OLD  38165  elghomlem2OLD  38166  isrngohom  38245  iscom2  38275  pridlval  38313  ispridl  38314  isdmn3  38354  inecmo  38635  islfl  39465  isopos  39585  psubspset  40149  islaut  40488  ispautN  40504  ltrnset  40523  isltrn  40524  istrnN  40562  istendo  41165  sticksstones1  42545  sticksstones2  42546  sticksstones3  42547  sticksstones8  42552  sticksstones10  42554  sticksstones11  42555  sticksstones12a  42556  sticksstones15  42560  sn-isghm  43060  clsk1independent  44431  relpeq1  45329  relpeq2  45330  relpeq3  45331  sprsymrelfolem2  47882  sprsymrelfo  47886  reuopreuprim  47915  dmatALTbasel  48791  lindslinindsimp2  48852  lmod1  48881  isnrm4  49319  iscnrm4  49342  isuplem  49567  isthinc  49807  thincciso  49841  thinccisod  49842