Theorem 2ralbidv 3229

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wral 3079

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This proof depends on definitions:  df-bi 210  df-an 401  df-ral 3080

This theorem is used by:  3ralbidv  3232  6ralbidv  3234  cbvral3vw  3249  cbvral6vw  3251  cbvral3v  3359  rspc6v  3602  ralxpxfr2d  3605  poeq1  5572  soeq1  5590  isoeq1  7315  isoeq2  7316  isoeq3  7317  fnmpoovd  8078  xpord3inddlem  8146  smoeq  8333  xpf1o  9123  nqereu  10918  dedekind  11377  dedekindle  11378  seqcaopr2  14079  wrd2ind  14765  addcn2  15650  mulcn2  15652  mreexexd  17708  catlid  17743  catrid  17744  isfunc  17925  funcres2b  17958  isfull  17973  isfth  17977  fullres2c  18002  isnat  18011  evlfcl  18282  uncfcurf  18299  isprs  18356  isdrs  18361  ispos  18374  istos  18476  resspos  18489  resstos  18490  isdlat  18582  ismgmhm  18758  issubmgm  18764  sgrp1  18791  ismhm  18847  issubm  18865  sgrp2nmndlem4  18994  isnsg  19225  isghm  19290  isga  19365  pmtrdifwrdel  19559  sylow2blem2  19695  efglem  19790  efgi  19793  efgredlemb  19820  efgred  19822  frgpuplem  19846  iscmn  19863  isomnd  20197  ring1  20398  isirred  20506  rnghmval  20527  isrnghm  20528  rhmval0  20562  isrhm0  20563  isorng  20973  islmod  20994  lmodlema  20995  lssset  21063  islssd  21065  islmhm  21157  islmhm2  21168  prmidlval  21471  isprmidl  21472  isobs  21879  dmatel  22659  dmatmulcl  22666  scmateALT  22678  mdetunilem3  22780  mdetunilem4  22781  mdetunilem9  22786  cpmatel  22877  chpscmat  23008  hausnei2  23519  dfconn2  23585  llyeq  23636  nllyeq  23637  isucn2  24444  iducn  24448  ispsmet  24470  ismet  24489  isxmet  24490  metucn  24737  ngptgp  24802  nlmvscnlem1  24852  xmetdcn2  25004  addcnlem  25031  elcncf  25057  ipcnlem1  25413  cfili  25436  c1lip1  26165  aalioulem5  26508  aalioulem6  26509  aaliou  26510  aaliou2  26512  aaliou2b  26513  ulmcau  26567  ulmdvlem3  26574  cxpcn3lem  26921  mpodvdsmulf1o  27367  dvdsmulf1o  27369  chpdifbndlem2  27727  pntrsumbnd2  27740  addsprop  28178  negsprop  28237  istrkgb  28733  axtgsegcon  28742  axtg5seg  28743  axtgpasch  28745  axtgeucl  28750  iscgrg  28790  isismt  28812  isperp2  29004  f1otrg  29229  axcontlem10  29332  axcontlem12  29334  iscusgredg  29782  isgrpo  30858  isablo  30907  vacn  31055  smcnlem  31058  lnoval  31113  islno  31114  isphg  31178  ajmoi  31219  ajval  31222  adjmo  32193  elcnop  32218  ellnop  32219  elunop  32233  elhmop  32234  elcnfn  32243  ellnfn  32244  adjeu  32250  adjval  32251  adj1  32294  adjeq  32296  cnlnadjlem9  32436  cnlnadjeu  32439  cnlnssadj  32441  isst  32574  ishst  32575  cdj1i  32794  cdj3i  32802  ismnt  33312  mgcval  33316  isslmd  33531  slmdlema  33532  isrprm  33816  qqhucn  34391  ismntop  34425  axtgupdim2ALTV  35064  txpconn  35732  nmulprop  36690  nmulr0  36695  nmuladdel  36712  ltnmul  36716  nn0prpw  36862  heicant  38334  equivbnd  38469  isismty  38480  heibor1lem  38488  iccbnd  38519  isass  38525  elghomlem1OLD  38564  elghomlem2OLD  38565  isrngohom  38644  iscom2  38674  pridlval  38712  ispridl  38713  isdmn3  38753  inecmo  39032  islfl  39862  isopos  39982  psubspset  40546  islaut  40885  ispautN  40901  ltrnset  40920  isltrn  40921  istrnN  40959  istendo  41562  sticksstones1  42941  sticksstones2  42942  sticksstones3  42943  sticksstones8  42948  sticksstones10  42950  sticksstones11  42951  sticksstones12a  42952  sticksstones15  42956  sn-isghm  43433  clsk1independent  44800  relpeq1  45681  relpeq2  45682  relpeq3  45683  sprsymrelfolem2  48270  sprsymrelfo  48274  reuopreuprim  48303  isidom3  49138  dmatALTbasel  49210  lindslinindsimp2  49271  lmod1  49300  isnrm4  49737  iscnrm4  49760  isuplem  49985  isthinc  50225  thincciso  50259  thinccisod  50260