Theorem reubii 3128

Description: Formula-building rule for restricted existential quantifier (inference rule). (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 3127	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 196   ∈ wcel 1990  ∃!wreu 2914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-eu 2474  df-reu 2919

This theorem is referenced by:  2reu5lem1  3413  reusv2lem5  4873  reusv2  4874  oaf1o  7643  aceq2  8942  lubfval  16978  lubeldm  16981  glbfval  16991  glbeldm  16994  oduglb  17139  odulub  17141  usgredg2vlem1  26117  usgredg2vlem2  26118  frcond1  27130  frcond2  27131  n4cyclfrgr  27155  cnlnadjlem3  28928  disjrdx  29404  lshpsmreu  34396  2reu7  41191  2reu8  41192