Theorem reubii 3353

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

Syntax hints:   ↔ wb 207   ∈ wcel 2119  ∃!wreu 3342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-mo 2543  df-eu 2573  df-reu 3345

This theorem is referenced by:  2reu5lem1  3696  reusv2lem5  5331  reusv2  5332  oaf1o  8488  aceq2  10032  lubfval  18305  lubeldm  18308  glbfval  18318  glbeldm  18321  odulub  18362  oduglb  18364  2sqreu  27437  2sqreunn  27438  2sqreult  27439  2sqreultb  27440  2sqreunnlt  27441  2sqreunnltb  27442  uspgredgiedg  29262  uspgriedgedg  29263  usgredg2vlem1  29312  usgredg2vlem2  29313  frcond1  30354  frcond2  30355  n4cyclfrgr  30379  cnlnadjlem3  32158  disjrdx  32680  ply1divalg3  35870  lshpsmreu  39601  reuf1odnf  47570  reuf1od  47571  2reu7  47574  2reu8  47575  2reu8i  47576  2reuimp0  47577  isuspgrim0  48385  isuspgrimlem  48386  uptr2  49711