Theorem eqrelriiv 5778

Description: Inference from extensionality principle for relations. (Contributed by NM, 17-Mar-1995.)

Hypotheses

Ref	Expression
eqreliiv.1	⊢ Rel 𝐴
eqreliiv.2	⊢ Rel 𝐵
eqreliiv.3	⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵)

Assertion

Ref	Expression
eqrelriiv	⊢ 𝐴 = 𝐵

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦

Proof of Theorem eqrelriiv

Step	Hyp	Ref	Expression
1		eqreliiv.1	. 2 ⊢ Rel 𝐴
2		eqreliiv.2	. 2 ⊢ Rel 𝐵
3		eqreliiv.3	. . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵)
4	3	eqrelriv 5777	. 2 ⊢ ((Rel 𝐴 ∧ Rel 𝐵) → 𝐴 = 𝐵)
5	1, 2, 4	mp2an 705	1 ⊢ 𝐴 = 𝐵

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2146  ⟨cop 4597  Rel wrel 5668

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  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3923  df-opab 5176  df-xp 5669  df-rel 5670

This theorem is used by:  eqbrriv  5779  inopab  5818  difopab  5819  inxp  5820  dfres2  6045  restidsing  6057  cnvopab  6139  cnvdif  6142  difxp  6163  cnvcnvsn  6222  dfco2  6248  coiun  6260  co02  6264  coass  6269  ressn  6290  ovoliunlem1  25714  h2hlm  31405  cnvco1  36290  cnvco2  36291  inxprnres  39007  cnviun  44436  coiun1  44438  coxp  49670