Theorem 2ralbii 3108

Description: Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)

Hypothesis

Ref	Expression
2ralbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
2ralbii	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Proof of Theorem 2ralbii

Step	Hyp	Ref	Expression
1		2ralbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	ralbii 3075	. 2 ⊢ (∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 𝜓)
3	2	ralbii 3075	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Syntax hints:   ↔ 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

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

This theorem is referenced by:  3ralbii  3110  ralnex3  3114  rmo4f  3703  2reu4lem  4481  cnvso  6249  fununi  6575  dff14a  7227  isocnv2  7288  f1opr  7425  sorpss  7684  xpord3inddlem  8110  tpossym  8214  dford2  9549  isffth2  17856  ispos2  18252  issubmgm  18605  issubm  18706  cntzrec  19244  oppgsubm  19270  opprirred  20307  opprsubrng  20444  rhmimasubrng  20451  cntzsubrng  20452  opprsubrg  20478  isdomn5  20595  isdomn3  20600  gsummatr01lem3  22520  gsummatr01  22522  isbasis2g  22811  ist0-3  23208  isfbas2  23698  isclmp  24973  addsproplem4  27855  addsproplem6  27857  addsprop  27859  negsproplem4  27913  negsproplem6  27915  negsprop  27917  mulsprop  28009  dfadj2  31787  adjval2  31793  cnlnadjeui  31979  adjbdln  31985  isarchi  33109  prmidl0  33394  ply1dg3rt0irred  33524  dff15  35047  iccllysconn  35210  dfso3  35680  elpotr  35742  dfon2  35753  idinxpss  38273  inxpssidinxp  38277  idinxpssinxp  38278  dfeldisj5  38686  isltrn2N  40087  hashnexinj  42089  fphpd  42777  fiinfi  43535  ntrk1k3eqk13  44012  ordelordALT  44500  dfac5prim  44953  disjinfi  45159  isthinc2  49382  isthinc3  49383