Theorem reubii 3375

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

Hypothesis

Ref	Expression
rmobii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

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

Proof of Theorem reubii

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145  ∃!wreu 3364

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2565  df-eu 2595  df-reu 3367

This theorem is used by:  2reu5lem1  3713  reusv2lem5  5364  reusv2  5365  oaf1o  8564  aceq2  10191  lubfval  18515  lubeldm  18518  glbfval  18528  glbeldm  18531  odulub  18572  oduglb  18574  2sqreu  27776  2sqreunn  27777  2sqreult  27778  2sqreultb  27779  2sqreunnlt  27780  2sqreunnltb  27781  uspgredgiedg  29749  uspgriedgedg  29750  usgredg2vlem1  29799  usgredg2vlem2  29800  frcond1  30860  frcond2  30861  n4cyclfrgr  30885  cnlnadjlem3  32664  disjrdx  33178  ply1divalg3  36386  lshpsmreu  40146  reuf1odnf  48146  reuf1od  48147  2reu7  48150  2reu8  48151  2reu8i  48152  2reuimp0  48153  isuspgrim0  48961  isuspgrimlem  48962  uptr2  50298  ralseubii  50898