Theorem vtoclbg 3502

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 346	. 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃)))
4		vtoclbg.3	. 2 ⊢ (𝜑 ↔ 𝜓)
5	3, 4	vtoclg 3500	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-clel 2814

This theorem is referenced by:  alexeqg  3589  pm13.183  3604  elab6g  3607  elabgw  3615  sbc8g  3731  sbc2or  3732  sbccow  3746  sbcco  3749  sbc5ALT  3752  sbcie2g  3763  eqsbc1  3769  sbcng  3770  sbcimg  3771  sbcan  3772  sbcor  3773  sbcbig  3774  sbcal  3782  sbcex2  3783  sbcel1v  3788  sbcreu  3808  csbiebg  3863  sbcel12  4339  sbceqg  4340  csbie2df  4371  preq12bg  4784  elintrabg  4891  sbcbr123  5126  inisegn0  6050  fsn2g  7080  funfvima3  7180  elixpsn  8875  ixpsnf1o  8876  domeng  8899  rankcf  10691  eldm3  35989  elima4  36004  brsset  36115  brbigcup  36124  elfix2  36130  elfunsg  36142  elsingles  36144  funpartlem  36170  ellines  36380  elhf2g  36404  bj-elpwgALT  37407  cover2g  38083