Theorem breldmg 3332

Description: Membership of first of a binary relation in a domain.

Assertion

Ref	Expression
breldmg	⊢ ((A ∈ C ⋀ ARB) → A ∈ dom R)

Proof of Theorem breldmg

Step	Hyp	Ref	Expression
1		breq1 2637	. . . 4 ⊢ (x = A → (xRB ↔ ARB))
2		eleq1 1541	. . . 4 ⊢ (x = A → (x ∈ dom R ↔ A ∈ dom R))
3	1, 2	imbi12d 629	. . 3 ⊢ (x = A → ((xRB → x ∈ dom R) ↔ (ARB → A ∈ dom R)))
4		visset 1820	. . . 4 ⊢ x ∈ V
5	4	breldm 3331	. . 3 ⊢ (xRB → x ∈ dom R)
6	3, 5	vtoclg 1854	. 2 ⊢ (A ∈ C → (ARB → A ∈ dom R))
7	6	imp 350	1 ⊢ ((A ∈ C ⋀ ARB) → A ∈ dom R)

Syntax hints:   → wi 3   ⋀ wa 223   = wceq 960   ∈ wcel 962   class class class wbr 2634  dom cdm 3186

This theorem is referenced by:  brelrng 3359  releldm 3362  fnbr 3606  pstr 8677

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-10 970  ax-12 972  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-10o 1144  ax-16 1214  ax-11o 1222  ax-ext 1464

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 985  df-sb 1176  df-clab 1470  df-cleq 1475  df-clel 1478  df-ne 1594  df-v 1819  df-dif 2060  df-un 2061  df-nul 2292  df-sn 2424  df-pr 2425  df-op 2428  df-br 2635  df-dm 3204

Copyright terms: Public domain