Theorem eqrelrdv2 5253

Description: A version of eqrelrdv 5250. (Contributed by Rodolfo Medina, 10-Oct-2010.)

Hypothesis

Ref	Expression
eqrelrdv2.1	⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵))

Assertion

Ref	Expression
eqrelrdv2	⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵)

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

Proof of Theorem eqrelrdv2

Step	Hyp	Ref	Expression
1		eqrelrdv2.1	. . . 4 ⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	alrimivv 1896	. . 3 ⊢ (𝜑 → ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		eqrel 5243	. . 3 ⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
4	2, 3	syl5ibr 236	. 2 ⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝜑 → 𝐴 = 𝐵))
5	4	imp 444	1 ⊢ (((Rel 𝐴 ∧ Rel 𝐵) ∧ 𝜑) → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383  ∀wal 1521   = wceq 1523   ∈ wcel 2030  ⟨cop 4216  Rel wrel 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621  df-opab 4746  df-xp 5149  df-rel 5150

This theorem is referenced by:  xpiindi  5290  fliftcnv  6601  dmtpos  7409  ercnv  7808  fpwwe2lem9  9498  invsym2  16470  eqbrrdv2  34467  dibglbN  36772  diclspsn  36800  dih1  36892  dihglbcpreN  36906  dihmeetlem4preN  36912  rfovcnvf1od  38615