Theorem vtoclbg 3519

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.)

Hypotheses

Ref	Expression
vtoclbg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
vtoclbg.2	⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
vtoclbg.3	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
vtoclbg	⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Distinct variable groups:   𝑥,𝐴   𝜒,𝑥   𝜃,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝑉(𝑥)

Proof of Theorem vtoclbg

Step	Hyp	Ref	Expression
1		vtoclbg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2		vtoclbg.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
3	1, 2	bibi12d 348	. 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃)))
4		vtoclbg.3	. 2 ⊢ (𝜑 ↔ 𝜓)
5	3, 4	vtoclg 3517	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145

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 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-clel 2835

This theorem is used by:  alexeqg  3605  pm13.183  3620  elab6g  3623  elabgw  3631  sbc8g  3747  sbc2or  3748  sbccow  3762  sbcco  3765  sbc5ALT  3768  sbcie2g  3779  eqsbc1  3785  sbcng  3786  sbcimg  3787  sbcan  3788  sbcor  3789  sbcbig  3790  sbcal  3798  sbcex2  3799  sbcel1v  3804  sbcreu  3823  csbiebg  3879  sbcel12  4369  sbceqg  4370  csbie2df  4401  preq12bg  4813  elintrabg  4921  sbcbr123  5159  inisegn0  6094  fsn2g  7133  funfvima3  7236  elixpsn  8945  ixpsnf1o  8946  domeng  8969  rankcf  10787  kardeng  35684  eldm3  36341  elima4  36356  brsset  36467  brbigcup  36476  elfix2  36482  elfunsg  36494  elsingles  36496  funpartlem  36522  ellines  36733  elhf2g  36757  bj-elpwgALT  37799  cover2g  38467