Theorem brerser 38781

Description: Binary equivalence relation with natural domain and the equivalence relation with natural domain predicate are the same when 𝐴 and 𝑅 are sets. (Contributed by Peter Mazsa, 25-Aug-2021.)

Assertion

Ref	Expression
brerser	⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Ers 𝐴 ↔ 𝑅 ErALTV 𝐴))

Proof of Theorem brerser

Step	Hyp	Ref	Expression
1		brers 38771	. . 3 ⊢ (𝐴 ∈ 𝑉 → (𝑅 Ers 𝐴 ↔ (𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴)))
2	1	adantr 480	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Ers 𝐴 ↔ (𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴)))
3		eleqvrelsrel 38696	. . . . 5 ⊢ (𝑅 ∈ 𝑊 → (𝑅 ∈ EqvRels ↔ EqvRel 𝑅))
4	3	adantl 481	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 ∈ EqvRels ↔ EqvRel 𝑅))
5		brdmqssqs 38750	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 DomainQss 𝐴 ↔ 𝑅 DomainQs 𝐴))
6	4, 5	anbi12d 632	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ((𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴) ↔ ( EqvRel 𝑅 ∧ 𝑅 DomainQs 𝐴)))
7		df-erALTV 38768	. . 3 ⊢ (𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ 𝑅 DomainQs 𝐴))
8	6, 7	bitr4di 289	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → ((𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴) ↔ 𝑅 ErALTV 𝐴))
9	2, 8	bitrd 279	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 Ers 𝐴 ↔ 𝑅 ErALTV 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2111   class class class wbr 5093   EqvRels ceqvrels 38244   EqvRel weqvrel 38245   DomainQss cdmqss 38251   DomainQs wdmqs 38252   Ers cers 38253   ErALTV werALTV 38254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-ec 8630  df-qs 8634  df-rels 38470  df-ssr 38596  df-refs 38608  df-refrels 38609  df-refrel 38610  df-syms 38640  df-symrels 38641  df-symrel 38642  df-trs 38674  df-trrels 38675  df-trrel 38676  df-eqvrels 38686  df-eqvrel 38687  df-dmqss 38740  df-dmqs 38741  df-ers 38767  df-erALTV 38768

This theorem is referenced by:  mpets2  38945  pets  38956