Theorem 2ralbidv 3201

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  3ralbidv  3204  6ralbidv  3206  cbvral3vw  3221  cbvral6vw  3223  cbvral3v  3344  rspc6v  3609  ralxpxfr2d  3612  poeq1  5549  soeq1  5567  isoeq1  7292  isoeq2  7293  isoeq3  7294  fnmpoovd  8066  xpord3inddlem  8133  smoeq  8319  xpf1o  9103  nqereu  10882  dedekind  11337  dedekindle  11338  seqcaopr2  14003  wrd2ind  14688  addcn2  15560  mulcn2  15562  mreexexd  17609  catlid  17644  catrid  17645  isfunc  17826  funcres2b  17859  isfull  17874  isfth  17878  fullres2c  17903  isnat  17912  evlfcl  18183  uncfcurf  18200  isprs  18257  isdrs  18262  ispos  18275  istos  18377  isdlat  18481  ismgmhm  18623  issubmgm  18629  sgrp1  18656  ismhm  18712  issubm  18730  sgrp2nmndlem4  18855  isnsg  19087  isghm  19147  isghmOLD  19148  isga  19223  pmtrdifwrdel  19415  sylow2blem2  19551  efglem  19646  efgi  19649  efgredlemb  19676  efgred  19678  frgpuplem  19702  iscmn  19719  ring1  20219  isirred  20328  rnghmval  20349  isrnghm  20350  islmod  20770  lmodlema  20771  lssset  20839  islssd  20841  islmhm  20934  islmhm2  20945  isobs  21629  dmatel  22380  dmatmulcl  22387  scmateALT  22399  mdetunilem3  22501  mdetunilem4  22502  mdetunilem9  22507  cpmatel  22598  chpscmat  22729  hausnei2  23240  dfconn2  23306  llyeq  23357  nllyeq  23358  isucn2  24166  iducn  24170  ispsmet  24192  ismet  24211  isxmet  24212  metucn  24459  ngptgp  24524  nlmvscnlem1  24574  xmetdcn2  24726  addcnlem  24753  elcncf  24782  ipcnlem1  25145  cfili  25168  c1lip1  25902  aalioulem5  26244  aalioulem6  26245  aaliou  26246  aaliou2  26248  aaliou2b  26249  ulmcau  26304  ulmdvlem3  26311  cxpcn3lem  26657  mpodvdsmulf1o  27104  dvdsmulf1o  27106  chpdifbndlem2  27465  pntrsumbnd2  27478  addsprop  27883  negsprop  27941  istrkgb  28382  axtgsegcon  28391  axtg5seg  28392  axtgpasch  28394  axtgeucl  28399  iscgrg  28439  isismt  28461  isperp2  28642  f1otrg  28798  axcontlem10  28900  axcontlem12  28902  iscusgredg  29350  isgrpo  30426  isablo  30475  vacn  30623  smcnlem  30626  lnoval  30681  islno  30682  isphg  30746  ajmoi  30787  ajval  30790  adjmo  31761  elcnop  31786  ellnop  31787  elunop  31801  elhmop  31802  elcnfn  31811  ellnfn  31812  adjeu  31818  adjval  31819  adj1  31862  adjeq  31864  cnlnadjlem9  32004  cnlnadjeu  32007  cnlnssadj  32009  isst  32142  ishst  32143  cdj1i  32362  cdj3i  32370  resspos  32892  resstos  32893  ismnt  32909  mgcval  32913  isomnd  33015  isslmd  33155  slmdlema  33156  isorng  33277  prmidlval  33408  isprmidl  33409  isrprm  33488  qqhucn  33982  ismntop  34016  axtgupdim2ALTV  34659  txpconn  35219  nn0prpw  36311  heicant  37649  equivbnd  37784  isismty  37795  heibor1lem  37803  iccbnd  37834  isass  37840  elghomlem1OLD  37879  elghomlem2OLD  37880  isrngohom  37959  iscom2  37989  pridlval  38027  ispridl  38028  isdmn3  38068  inecmo  38337  islfl  39053  isopos  39173  psubspset  39738  islaut  40077  ispautN  40093  ltrnset  40112  isltrn  40113  istrnN  40151  istendo  40754  sticksstones1  42134  sticksstones2  42135  sticksstones3  42136  sticksstones8  42141  sticksstones10  42143  sticksstones11  42144  sticksstones12a  42145  sticksstones15  42149  sn-isghm  42661  clsk1independent  44035  relpeq1  44934  relpeq2  44935  relpeq3  44936  sprsymrelfolem2  47494  sprsymrelfo  47498  reuopreuprim  47527  dmatALTbasel  48391  lindslinindsimp2  48452  lmod1  48481  isnrm4  48919  iscnrm4  48942  isuplem  49168  isthinc  49408  thincciso  49442  thinccisod  49443