Theorem reubii 3344

Description: Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 22-Oct-1999.)

Hypothesis

Ref	Expression
reubii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
reubii	⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓)

Proof of Theorem reubii

Step	Hyp	Ref	Expression
1		reubii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))
3	2	reubiia 3343	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 209   ∈ wcel 2111  ∃!wreu 3108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-mo 2598  df-eu 2629  df-reu 3113

This theorem is referenced by:  2reu5lem1  3694  reusv2lem5  5268  reusv2  5269  oaf1o  8172  aceq2  9530  lubfval  17580  lubeldm  17583  glbfval  17593  glbeldm  17596  oduglb  17741  odulub  17743  2sqreu  26040  2sqreunn  26041  2sqreult  26042  2sqreultb  26043  2sqreunnlt  26044  2sqreunnltb  26045  usgredg2vlem1  27015  usgredg2vlem2  27016  frcond1  28051  frcond2  28052  n4cyclfrgr  28076  cnlnadjlem3  29852  disjrdx  30354  lshpsmreu  36405  reuf1odnf  43663  reuf1od  43664  2reu7  43667  2reu8  43668  2reu8i  43669  2reuimp0  43670