Theorem reubii 3355

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 3353	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 206   ∈ wcel 2111  ∃!wreu 3344

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-mo 2535  df-eu 2564  df-reu 3347

This theorem is referenced by:  2reu5lem1  3709  reusv2lem5  5335  reusv2  5336  oaf1o  8473  aceq2  10005  lubfval  18249  lubeldm  18252  glbfval  18262  glbeldm  18265  odulub  18306  oduglb  18308  2sqreu  27389  2sqreunn  27390  2sqreult  27391  2sqreultb  27392  2sqreunnlt  27393  2sqreunnltb  27394  uspgredgiedg  29148  uspgriedgedg  29149  usgredg2vlem1  29198  usgredg2vlem2  29199  frcond1  30238  frcond2  30239  n4cyclfrgr  30263  cnlnadjlem3  32041  disjrdx  32563  ply1divalg3  35678  lshpsmreu  39148  reuf1odnf  47138  reuf1od  47139  2reu7  47142  2reu8  47143  2reu8i  47144  2reuimp0  47145  isuspgrim0  47925  isuspgrimlem  47926  uptr2  49253